PLMMS 2013 Workshop

• Deadline extension! Submission open until 27th May ATOE.
• Invited speakers confirmed! Titles and abstracts below.
• Workshop day confirmed as Tuesday 9th July 2013.
• Now accepting submissions via easychair.

Invited Speakers

• Edwin Brady -- Dependently Typed Functional Programming in Idris
  Idris is a general purpose pure functional programming language with dependent types. Its syntax is influenced by Haskell and its features include full dependent types and records, type classes, tactic based theorem proving, totality checking and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to functional programmers while still supporting efficient systems programming via an optimising compiler and interaction with external libraries. In this talk I will introduce dependently typed programming using Idris, and demonstrate its features using several examples including an interpreter for the simply typed lambda calculus, and a verified binary adder.

• Gilles Dowek -- Checking classical proofs in an constructive proof-checker
  The Dedukti project aims at using a single proof-checker to check proofs developed in many other provers. As some of these provers are classical and other constructive, we need a way to express proofs of one logic into the other. In this talk I will sketch various ways to express classical proofs in a constructive setting, focussing on the possibility to design a single logic mixing classical and constructive connectors and on the possibility to recognize classical proofs that are constructive by chance. This talk will be based on joint work with Olivier Hermant and Frédéric Gilbert.

• Conor McBride -- Problems as types
  Abstract to be confirmed

• Sergei Meshveliani -- Dependent Types for an Adequate Programming of Algebra
  This research compares the author's experience in programming algebra in Haskell and in Agda (currently the former experience is large, and the latter is small). There are discussed certain hopes and doubts related to the dependently typed and verified programming of symbolic computation. This concerns the 1) author's experience history, 2) algebraic class hierarchy design, 3) proof cost overhead in evaluation and in coding, 4) other subjects. Various examples are considered, some questions are put.

Workshop Topics

• Input languages for MMS: all aspects of languages for the user to deploy or extend the system, both algorithmic and declarative. Typical examples are tactic languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, and specialized programming languages built into CA systems.
• Mathematical modelling languages used for programming: the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational worldview?
• Programming languages and mathematical specifications: advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality.
• Language elements for program verification: specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How can MMS and PL be improved to make verification more convenient and mathematically appealing?

Important Dates:

Program Committee:

• David Aspinall, University of Edinburgh, UK
• Serge Autexier, DFKI Bremen, Germany
• Jacques Carette, McMaster University, Canada
• Claudio Sacerdoti Coen, University of Bologna, Italy
• Gudmund Grov, Heriot Watt University, UK
• Cezar Ionescu, Potsdam Institute, Germany
• Ewen Maclean, University of Edinburgh, UK
• Florian Rabe (co-chair), Jacobs University, Germany
• Tim Sheard, Portland State University, USA
• Sergei Soloviev, IRIT, France
• Stephen Watt, University of Western Ontario, Canada
• Makarius Wenzel, Université Paris-Sud, France
• Iain Whiteside (co-chair), University of Newcastle, UK
• Freek Wiedijk, Radboud University, Netherlands
• Wolfgang Windsteiger, RISC, Austria