You can subscribe to this list here.
2007 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(2) 
_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}


2008 
_{Jan}

_{Feb}
(1) 
_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(1) 
_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(2) 
2009 
_{Jan}
(2) 
_{Feb}
(3) 
_{Mar}
(1) 
_{Apr}
(3) 
_{May}

_{Jun}

_{Jul}

_{Aug}
(1) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

2010 
_{Jan}
(4) 
_{Feb}

_{Mar}
(3) 
_{Apr}

_{May}

_{Jun}
(1) 
_{Jul}
(1) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2011 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}
(1) 
_{Aug}

_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}

2012 
_{Jan}
(1) 
_{Feb}
(1) 
_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}
(1) 
_{Apr}

_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 




1

2

3
(1) 
4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23
(1) 
24

25

26

27

28
(1) 
29

30



From: Gabriel Dos Reis <gdr@cs...>  20090428 09:48:17

The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be colocated with TPHOLs 2009. Important Dates * Abstract submission : May 11, 2009 (Apia, Samoa time) * Submission deadline: May 18, 2009 (Apia, Samoa time) * Author notification: June 22, 2009 * Camera ready papers: July 10, 2009 * Workshop: August 21, 2009 General Information The scope of this workshop is at 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. 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 world view? * 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. 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. 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? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (CoChair) * JeanChristophe 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 (CoChair) * Makarius Wenzel, Technische Universität München 
From: Gabriel Dos Reis <gdr@cs...>  20090423 17:48:54

FYI. From: John R Harrison <johnh@...> Subject: My automated theorem proving textbook is now available Date: Tue, 21 Apr 2009 20:35:50 0700 For some time I've been working on a textbook giving a survey of some of the main results in automated theorem proving together with an introduction to basic mathematical logic. All the automated theorem proving techniques described are accompanied by actual OCaml code that the reader can use, modify and otherwise experiment with. I'm pleased to announce that the book has now been published. Handbook of Practical Logic and Automated Reasoning John Harrison Cambridge University Press 2009 ISBN: 9780521899574 Publisher's Web page: http://www.cambridge.org/9780521899574 Code and resources: http://www.cl.cam.ac.uk/~jrh13/atp/ Copies are already becoming available: you can order it directly from the publisher or from various other sources. Currently the price and availability looks a bit better in Europe (it was on offer for 56 pounds last week on amazon.co.uk). Here's a table of contents: 1 Introduction 1.1 What is logical reasoning? 1.2 Calculemus! 1.3 Symbolism 1.4 Boole's algebra of logic 1.5 Syntax and semantics 1.6 Symbolic computation and OCaml 1.7 Parsing 1.8 Prettyprinting 2 Propositional Logic 2.1 The syntax of propositional logic 2.2 The semantics of propositional logic 2.3 Validity, satisfiability and tautology 2.4 The De Morgan laws, adequacy and duality 2.5 Simplification and negation normal form 2.6 Disjunctive and conjunctive normal forms 2.7 Applications of propositional logic 2.8 Definitional CNF 2.9 The DavisPutnam procedure 2.10 Staalmarck's method 2.11 Binary Decision Diagrams 2.12 Compactness 3 Firstorder logic 3.1 Firstorder logic and its implementation 3.2 Parsing and printing 3.3 The semantics of firstorder logic 3.4 Syntax operations 3.5 Prenex normal form 3.6 Skolemization 3.7 Canonical models 3.8 Mechanizing Herbrand's theorem 3.9 Unification 3.10 Tableaux 3.11 Resolution 3.12 Subsumption and replacement 3.13 Refinements of resolution 3.14 Horn clauses and Prolog 3.15 Model elimination 3.16 More firstorder metatheorems 4 Equality 4.1 Equality axioms 4.2 Categoricity and elementary equivalence 4.3 Equational logic and completeness theorems 4.4 Congruence closure 4.5 Rewriting 4.6 Termination orderings 4.7 KnuthBendix completion 4.8 Equality elimination 4.9 Paramodulation 5 Decidable problems 5.1 The decision problem 5.2 The AE fragment 5.3 Miniscoping and the monadic fragment 5.4 Syllogisms 5.5 The finite model property 5.6 Quantifier elimination 5.7 Presburger arithmetic 5.8 The complex numbers 5.9 The real numbers 5.10 Rings, ideals and word problems 5.11 Groebner bases 5.12 Geometric theorem proving 5.13 Combining decision procedures 6 Interactive theorem proving 6.1 Humanoriented methods 6.2 Interactive provers and proof checkers 6.3 Proof systems for firstorder logic 6.4 LCF implementation of firstorder logic 6.5 Propositional derived rules 6.6 Proving tautologies by inference 6.7 Firstorder derived rules 6.8 Firstorder proof by inference 6.9 Interactive proof styles 7 Limitations 7.1 Hilbert's programme 7.2 Tarski's theorem on the undefinability of truth 7.3 Incompleteness of axiom systems 7.4 Goedel's incompleteness theorem 7.5 Definability and decidability 7.6 Church's theorem 7.7 Further limitative results 7.8 Retrospective: the nature of logic John Harrison. 
From: Gabriel Dos Reis <gdr@cs...>  20090403 11:40:58

The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be colocated with TPHOLs 2009. General Information The scope of this workshop is at 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. 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 world view? * 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. 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. 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? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details * Submission deadline: May 11, 2009 (Apia, Samoa time) * Author Notification: June 22, 2009 * Final Papers Due: July 10, 2009 * Workshop: August 21, 2009 Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (CoChair) * JeanChristophe Filliâtre, CNRS Université Paris Sud * Predrag Janinic, University of Belgrade * Jaakko Järvi, Texas A&M University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (CoChair) * Makarius Wenzel, Technische Universität München 