FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

A
Abella	Computation-as-deduction in Abella: work in progress Functional programming with λ-tree syntax: a progress report
Abstract Syntax	What Does This Notation Mean Anyway? BNF-style notation as it is actually used
B
Barendregt's Variable Convention	Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
binder mobility	Functional programming with λ-tree syntax: a progress report
Binders	Abstract Representation of Binders in OCaml using the Bindlib Library
C
computation and deduction	Computation-as-deduction in Abella: work in progress
Constructive Type Theory	Formalization in Constructive Type Theory of the Standardization Theorem
Coq	Sharing a library between proof assistants: reaching out to the HOL family
D
Dedukti	Sharing a library between proof assistants: reaching out to the HOL family
E
exhaustive and randomized data generation	Property-Based Testing of Abstract Machines: an Experience Report
F
Formal Definition	What Does This Notation Mean Anyway? BNF-style notation as it is actually used
Formal Metatheory	Formalisation of Barendregt's Variable Convention for Generic Structures with Binders Formalization in Constructive Type Theory of the Standardization Theorem
functional and relational specifications	Computation-as-deduction in Abella: work in progress
functional programming	Functional programming with λ-tree syntax: a progress report
G
Generic Binding Structures	Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
H
Higher-order abstract syntax (HOAS)	Abstract Representation of Binders in OCaml using the Bindlib Library
HOL	Sharing a library between proof assistants: reaching out to the HOL family
I
Interoperability	Sharing a library between proof assistants: reaching out to the HOL family
L
lambda calculus	Formalization in Constructive Type Theory of the Standardization Theorem
lambda-tree syntax	Functional programming with λ-tree syntax: a progress report
Logical Frameworks	Sharing a library between proof assistants: reaching out to the HOL family
M
Matita	Sharing a library between proof assistants: reaching out to the HOL family
mechanized meta-theory	Property-Based Testing of Abstract Machines: an Experience Report
N
notation	What Does This Notation Mean Anyway? BNF-style notation as it is actually used
O
OCaml library	Abstract Representation of Binders in OCaml using the Bindlib Library
OpenTheory	Sharing a library between proof assistants: reaching out to the HOL family
P
property-based testing	Property-Based Testing of Abstract Machines: an Experience Report
S
Set Theory	What Does This Notation Mean Anyway? BNF-style notation as it is actually used
T
typed assembly languages	Property-Based Testing of Abstract Machines: an Experience Report

Disclaimer | Powered by EasyChair Smart Program