*** Call for participation ***

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

Vancouver, 22 June 2019 --- Affiliated with LICS 2019

Workshop page:       https://lfmtp.org/workshops/2019

Registration page:   

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

*** Workshop Programme ***

The program is available at


*** Invited speakers ***

Chris Hawblitzel (Systems Research Group, Microsoft Research, Redmond, USA)
Combining tactics, normalization, and SMT solving to verify systems software

Brigitte Pientka (McGill University, Canada)
Cocon: A Type Theory for Defining Logics and Proofs

*** Contributed talks ***

Michael Kohlhase and Jan Frederik Schaefer
GF + MMT = GLF - From Language to Semantics through LF

Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell and 
Marina Lenisa
A definitional implementation of the Lax Logical Framework LLFP in Coq

Dennis Müller and Florian Rabe
Rapid Prototyping Formal Systems in MMT: 5 Case Studies

François Thiré
Cumulative Types Systems and levels

Aaron Stump
Towards Higher-Order Abstract Syntax in Cedille

*** Programme committee ***

Danel Ahman (University of Ljubljana, Slovenia)
Amy Felty (University of Ottawa, Canada)
James Murdoch Gabbay (Heriot-Watt University, UK)
Daniel Hirschkoff (ENS Lyon, France)
Ralph Matthes (IRIT-Université Paul Sabatier, France)
Dale Miller (Inria-Saclay and LIX Ecole Polytechnique, France), co-chair
Elaine Pimentel (Federal University of Rio Grande do Norte, Brazil)
Florian Rabe (University of Paris South, France)
Ivan Scagnetto (University of Udine, Italy), co-chair
Gert Smolka (Saarland University, Germany)
Kristina Sojakova (Cornell University, USA)
Enrico Tassi (Inria-Sophia, France)

*** Contact ***

The organisers can be reached by email directly or via


Dale Miller (Inria-Saclay and LIX Ecole Polytechnique, France)
Ivan Scagnetto (University of Udine, Italy)

hol-info mailing list

Reply via email to