posted by user: Yoric || 2725 views || tracked by 4 users: [display]

PLMMS 2008 : Programming Languages for Mechanized Mathematics Systems

FacebookTwitterLinkedInGoogle

Link: http://events.cs.bham.ac.uk/cicm08/workshops/plmms/index.php
 
When Jul 28, 2008 - Jul 29, 2008
Where Birmingham, UK
Submission Deadline May 5, 2008
Notification Due Jun 6, 2008
Categories    programming languages   logics
 

Call For Papers

This workshop is focused on 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 that are expected to emerge eventually (cf. the objective of Calculemus).

The two subjects of PL and MMS meet in the following topics, which are of particular interest to this workshop:

* 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. Of particular interest are the semantics of those languages, especially when current ones are untyped.
* 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?

These issues have a very colorful history. Many PL innovations first appeared in either CA or proof systems first, before migrating into more mainstream programming languages. Some examples include type inference, dependent types, generics, term-rewriting, first-class types, first-class expressions, first-class modules, code extraction etc. However, such innovations were never aggressively pursued by builders of MMS, but often reconstructed by programming language researchers. This workshop is an opportunity to present the latest innovations in MMS design that may be relevant to future programming languages, or conversely novel PL principles that improve upon implementation and deployment of MMS.

We also want to critically examine what has worked, and what has not. Why are all the languages of mainstream CA systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modeling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers to using a more mainstream language as a host language for a CAS or PA/ATP?

Related Resources

ASPLOS 2025   The ACM International Conference on Architectural Support for Programming Languages and Operating Systems
IJPLA 2024   International Journal of Programming Languages and Applications
OOPSLA 2024   The Object-Oriented Programming, Systems, Languages, and Applications 2024 (R2)
IJFLS 2024   International Journal of Fuzzy Logic Systems
NYC-2024-SE 2024   New York Annual Conference on Software Engineering 2024
APL 2024   Advances in Programming Languages (APL) Thematic Track at the 19th Conference on Computer Science and Intelligence Systems (FedCSIS 2024)
ASPLOS 2025   The ACM International Conference on Architectural Support for Programming Languages and Operating Systems
ECOOP (R2) 2024   European Conference on Object-Oriented Programming
APLAS 2024   The 22nd Asian Symposium on Programming Languages and Systems
PPDP 2024   The 26th International Symposium on Principles and Practice of Declarative Programming