PLMMS 2013 Workshop
News!

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.
The Programming Languages for Mechanized
Mathematics Systems (PLMMS) workshop brings together researchers from programming languages and mechanized mathematics systems, who share the vision of comprehensive mechanized mathematical assistant systems.
The scope of this workshop is the intersection of programming
languages (PL) and mechanized mathematics systems (MMS).
The latter category subsumes presentday computer algebra
systems (CAS), interactive proof assistants (PA), and automated
theorem provers (ATP), all heading towards fully integrated
mechanized mathematical assistants.
We hope to have four invited speakers this year:

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 typebased 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 proofchecker
The Dedukti project aims at using a single proofchecker 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
The topics of interest meet at, but are not limited to,
the following:
 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:
Paper submission:  27 May 2013 
Notification of acceptance:  10 June 2013 
Camera ready copy:  17 June 2013 
Workshop Day:  Tuesday 9th July 
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 (cochair), Jacobs University, Germany

Tim Sheard, Portland State University, USA

Sergei Soloviev, IRIT, France

Stephen Watt, University of Western Ontario, Canada

Makarius Wenzel, Université ParisSud, France

Iain Whiteside (cochair), University of Newcastle, UK

Freek Wiedijk, Radboud University, Netherlands

Wolfgang Windsteiger, RISC, Austria
