Last update: 4 July 2018
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
LFMTP 2018 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
- Encoding and reasoning about the meta-theory of programming languages, logical systems and related formally specified systems.
- Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.
- Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory.
- Graphical languages for building proofs, applications in geometry, equational reasoning and category theory.
- New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory.
- Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc.
- Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog.
Venue
Lecture Theatre 2, Mathematical Institute, Radcliffe Observatory Quarter, Woodstock Road.
Program
See the program.
Registration
See FLoC registration website. The deadline for early registration is June 6th.
LFMTP dinner
LFMTP will organize a dinner after the workshop (apart from the FLOC workshop dinner). If you want to join, please send a mail before July 1st.
Invited Speakers
- Delia Kesner (IRIF, CNRS and Université Paris Diderot, France)
- Kuen-Bang Hou, alias Favonia (Institute for Advanced Study, Princeton, USA)
- Grigore Rosu (University of Illinois at Urbana-Champaign, USA)
For information about titles and abstracts, see Invited Talks.
List of accepted papers
Regular papers [EPTCS proceedings]
- Formalization in Constructive Type Theory of the Standardization Theorem, by Martin Copes, Nora Szasz and Alvaro Tasistro
- Formalisation of Barendregt's Variable Convention for Generic Structures with Binders, by Ernesto Copello, Nora Szasz and Alvaro Tasistro
- Sharing a library between proof assistants: reaching out to the HOL family, by François Thiré
- Abstract Representation of Binders in OCaml using the Bindlib Library, by Rodolphe Lepigre and Christophe Raffalli
Work-in-progress or experience reports [HAL proceedings]
- What Does This Notation Mean Anyway? by David Feller, Joe Wells, Sébastien Carlier and Fairouz Kamareddine
- Property-Based Testing Abstract Machines: an Experience Report, by Francesco Komauli and Alberto Momigliano
- Computation-as-deduction in Abella: work in progress, by Kaustuv Chaudhuri, Ulysse Gérard and Dale Miller
- Functional programming with λ-tree syntax: a progress report, by Ulysse Gérard and Dale Miller
Important Dates
- Sunday, April 22th: Abstract submission deadline
- Sunday, April 29th: Submission deadline
- Saturday, May 19th: Notification to authors
- Monday, May 28th: Final version due
- Saturday, July 7th: Workshop
Submission
In addition to regular papers, we accept the submission of "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be of interest for the community at large.
Submitted papers should be in PDF, formatted using the EPTCS style guidelines. The length is restricted to 15 pages for regular papers and 8 pages for "Work in Progress" papers.
Submission is via EasyChair.
Proceedings
Regular papers are published in the volume 274 of the Electronic Proceedings in Theoretical Computer Science (EPTCS). Works in progress and experience reports are published online in HAL.
Program Committee
- María Alpuente (Universitat Politècnica de València, Spain)
- Andrej Bauer (University of Ljubljana, Slovenia)
- Frédéric Blanqui (Inria, France), co-chair
- Ana Bove (Chalmers University of Technology, Sweden)
- Stéphane Graham-Lengrand (CNRS, France)
- Makoto Hamana (Gunma University, Japan)
- Chantal Keller (Université Paris-Sud, France)
- Carlos Olarte (Universidade Federal do Rio Grande do Norte, Brazil)
- Giselle Reis (CMU, Qatar), co-chair
- Aaron Stump (University of Iowa, USA)
- Yuting Wang (Yale University, USA)