coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ivan Scagnetto <ivan.scagnetto AT uniud.it>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] LFMTP 2019 - Call for participation
- Date: Tue, 4 Jun 2019 06:58:07 +0000
- Accept-language: it-IT, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ivan.scagnetto AT uniud.it; spf=Pass smtp.mailfrom=ivan.scagnetto AT uniud.it; spf=Pass smtp.helo=postmaster AT EUR03-VE1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:fXEyfB3MXv1T2x3DsmDT+DRfVm0co7zxezQtwd8ZseMUKfad9pjvdHbS+e9qxAeQG9mCsrQd0Lqd6vm7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCegbb9oMRm7owbcusYLjYd/JKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJ/34DaboKUNPVica3ScsgXRXZYXspNSyBNHp+wY5YJAuEcPehYtY79p14WoBW9GwmjHuXvwSJViHDqx6I63OIhHh/a3Aw8GNIFrXPZrNTrNKgIV+C51rLIwinZYPNZ3zfy9pTIcgwmofyXQLJwd8vRyVQyGA/fj1WQtZXoMjWI3eoDtGib6vBvVeOpi2M/sAFxrCWvyt0whYbTno4Vzl7E9SBlwIYtP9G4T1R7YdGiHZBNtC+aL5N7T8w+T21ypSo21r8LtYS7cSQQyZkqyAbTZ+GHfoWL+B7vSfudLStiiH54d7+yiAy+/VW+xuDyTsW03khFoylZntTJs30CygDc58qDR/Z4/kquxyiD2gLW5+5aPUw4iaXWJps7zbEtipUetULOFTLslkrslq+ZbEAk9/Co6+v5ZrXmoYeROYB6hQ/iLqgjlNWzDus3PAQTRmSb/v+z26P58U3+XbVKkuY5kq7EsJDcOMsXvLa5AxVS0oY/9RmwEyum0NUfnXkBNl5Ffw+Hj5TtO1HJJ/D4Du2zjEirkDdu3/zGP7vhDYvRLnXbn7rtYaxx51NAxAcx19xS54hYB7AOLf7rX0/+rt3YDhs3MwyuxObnDc1w1oIAWW2VBK+VKrjSvkOS6eIgJemDepMVuCr6K/U++v7ui345mUIAcqWz3JsXdGi0Hu56LEWBfXrsntABHH8WsQo5VezmkUGNUTpOZ3mpRK88/TE6CIe+DYjZXIytgbqB3D26HpJMfGxGBEqMQj/UcNDOUPAVLSmWP8VJkzoeVLHnRZVrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQT6zVyR/+W2m6LQn1omStcRiE/2uZkqkVyzFqfza9QnvpZCNAV5u8fAVRyDoLV0+EvU4O6YQnGZNrcEA/3EOXjOik4S5cK+/FLZk98H9u4iRWah3i3Bb4Im/qKGM5tq/6O7z3KP894jk3++uw5lVB/GplSM2y7iuh+61qLXtObowCij6+vMJ8k8mvN+WOEkTXckXxiCFU1b4icGHcVaw3RsMjz4V7EQ/m2E7M7PwBdyMmEbKxXdtnuilYAT/Dmao3T
*** 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)
- [Coq-Club] LFMTP 2019 - Call for participation, Ivan Scagnetto, 06/04/2019
Archive powered by MHonArc 2.6.18.