[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

                                    *** Call for participation ***

*** LFMTP 2017: 19th Int. Workshop on Logical Frameworks and Meta-Languages: 
Theory and Practice  ***

Oxford, 8 September 2017 --- Affiliated with FSCD 2017

Workshop page:       http://lfmtp.org/workshops/2017

Registration page:   

LFMTP 2017 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 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.

- New theory contributions such as canonical and substructural frameworks, 
contextual frameworks, proof-theoretic foundations supporting binders, 
functional programming over logical frameworks, or homotopy type theory.

- Systematic translation, combination, and integration of logics or theorem 
prover libraries.

- Applications of logical frameworks, e.g. in certification and guarantee of 
security properties.

- 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.

LFMTP 2017 will be also the occasion to celebrate the 70th birthday of Randy 
Pollack, author of the LEGO proof assistant and many other contributions to 
this field.

*** Workshop Programme ***

The program is available at




*** Invited speakers ***

Andrew Appel

Verifiable C, a Higher-order Impredicative Concurrent Separation Logic in Coq

James McKinna

Names, Places, and Things; fragments of a partial intellectual biography of 
Randy Pollack

*** Contributed talks ***

Andreas Abel, Alberto Momigliano and Brigitte Pientka

POPLMark Reloaded

Jeff Polakow

Uniform Atomic Ordered Linear Logic

Claude Stolze, Luigi Liquori, Furio Honsell and Ivan Scagnetto

Towards a Logical Framework with Intersection and Union Types

Yuito Murase

Kripke-Style Contextual Modal Type Theory

Roberto Blanco, Dale Miller and Alberto Momigliano

Property-Based Testing via Proof Reconstruction: Work-in-progress

Michael D. Ariotti and John Tang Boyland

Making Substitutions Explicit in SASyLF

Jonas Kaiser, Steven Schäfer and Kathrin Stark

Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector 

Randy Pollack

Beta reduction without rule ξ

*** Programme committee ***

Thorsten Altenkirch (University of Nottingham, UK)

Kaustuv Chaudhuri (INRIA, France)

Gilles Dowek (ENS Cachan, France)

Amy Felty (University of Ottawa, Canada)

Andrzej Filinski (University of Copenhagen, Denmark)

Marino Miculan (DMIF, University of Udine, Italy),  co-chair

Florian Rabe (Jacobs University Bremen, Germany), co-chair

Wilmer Ricciotti (LFCS, University of Edinburgh, UK)

Claudio Sacerdoti Coen (University of Bologna, Italy)

Kristina Sojakova (Appalachian State University, USA)

*** Contact ***

The organisers can be reached by email directly or via


Florian Rabe (Jacobs University Bremen, Germany)

Marino Miculan (DMIF, University of Udine, Italy)

Reply via email to