[TYPES/announce] LFMTP 2017: Call for Participation

[Marino Miculan]

                                    *** 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:   http://www.cs.ox.ac.uk/conferences/fscd2017/registration.html



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

  http://lfmtp.org/workshops/2017/program.shtml

or

  http://www.cs.ox.ac.uk/conferences/fscd2017/programme.html



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


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


 lfmtp2017 at easychair.org


Florian Rabe (Jacobs University Bremen, Germany)

Marino Miculan (DMIF, University of Udine, Italy)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170809/dc1efafb/attachment-0001.html>