Registration for the PLMMS 2009 workshop is now open.
Important Dates and Deadlines
- Abstract submission: Now closed
- Submission deadline: Now closed
- Author notification: June 22, 2009
- Camera ready papers: July 15, 2009
- Registration: August 2, 2009
- Workshop: August 21, 2009
Online ProceedingsAn electronic copy of the proceedings is available here.
The scope of this workshop is at the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes present-day computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to:
- Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems.
- Mathematical modeling languages used for programming: covers 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 with mathematical specifications: covers 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: covers 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 need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way?
Friday, August 21
|09:00-10:00||Invited talk (Session Chair:)|
|Georges Gonthier. Ssreflect: Structured Scripting for Higher-Order Theorem Proving|
|10:40-12:10||Session 1 (Session Chair:)|
|Paulo F. Silva, Joost Visser, Jose Oliveira. Galois: A Language for Proofs Using Galois Connections and Fork Algebras|
|Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar|
|Andrea Asperti, Wilmer Riccioti, Claudio Sacerdoti Coen, Enrico Tassi. A New Type for Tactics|
|13:40-14:40||Invited tutorial (Session Chair:)|
|Gabriel Dos Reis. OpenAxiom: A Categorial Platform for Scientific Computation|
|15:10-16:10||Session 2 (Session Chair:)|
|Joe Hurd. OpenTheory: Package Management for Higher Order Logic Theories|
|Johannes Holzl. Proving Inequalities Over Reals With Computation in Isabelle/HOL|
- http://plmms09.cs.tamu.edu/, the PLMMS 2009 workshop web site
- http://tphols.in.tum.de/, the THOPLs 2009 conference web site
- Clemens Ballarin, aicas GmbH
- Gabriel Dos Reis, Texas A&M University (Co-Chair)
- Jean-Christophe Filliâtre, CNRS Université Paris Sud
- Predrag Janicic, University of Belgrade
- Jaakko Järvi, Texas A&M University
- Florina Piroi, Johannes Kepler University
- Laurent Théry, INRIA Sophia Antipolis (Co-Chair)
- Makarius Wenzel, Technische Universität München