[TYPES/announce] LFMTP 2019 - Call for participation

[Ivan Scagnetto]

                                    *** 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:   https://ungerboeck.its.sfu.ca/emc00/register.aspx?OrgCode=01&EvtID=132686&AppCode=REG&CC=119040326516


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

  https://lfmtp.org/workshops/2019/program.shtml


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

 lfmtp2019 at easychair.org

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