*** 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 lfmtp2...@easychair.org Dale Miller (Inria-Saclay and LIX Ecole Polytechnique, France) Ivan Scagnetto (University of Udine, Italy) _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info