posted by user: smwatt || 757 views || tracked by 2 users: [display]

PLMMS 2010 : Programming Languages for Mechanized Mathematics Systems

FacebookTwitterLinkedInGoogle

Link: http://dream.inf.ed.ac.uk/events/plmms-2010/
 
When Jul 8, 2010 - Jul 8, 2010
Where Paris, France
Abstract Registration Due Mar 26, 2010
Submission Deadline Apr 9, 2010
Notification Due May 24, 2010
Final Version Due Jun 7, 2010
 

Call For Papers

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. The program committee welcomes submissions on all aspects of programming languages and mechanised mathematics that meet, but not limited to, the following 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 modeling 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?

Related Resources

ASPLOS 2021   Architectural Support for Programming Languages and Operating Systems
LCPC 2020   Languages and Compilers for Parallel Computing
COMIT 2020   4th International Conference on Computer Science and Information Technology
PADL 2021   23rd International Symposium on Practical Aspects of Declarative Languages
COMPUTATION TOOLS 2020   The Eleventh International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking
ITCCMA 2020   7th International Conference on Information Technology, Control, Chaos, Modeling and Applications
SBLP 2020   24th Brazilian Symposium on Programming Languages
IFL 2020   IFL 2020: The 32nd Symposium on Implementation and Application of Functional Languages
POPL 2021   Principles of Programming Languages 2021
PLAS 2020   ACM SIGSAC Workshop on Programming Languages and Analysis for Security