FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program