Jacques Carette | 12 Mar 22:17 2007

CFP: Programming Languages for Mechanized Mathematics Workshop

[This might be of interest to the general Epigram community, if for no other reason than Epigram is mentioned in the CFP.  James McKinna has tentatively agreed for be on the PC, but I am awaiting final confirmation.]

Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007 Hagenberg, Austria


The intent of this workshop is to examine more closely the intersection between programming languages and mechanized mathematics systems (MMS). By MMS, we understand computer algebra systems (CAS), [automated] theorem provers (TP/ATP), all heading towards the development of fully unified systems (the MMS), sometimes also called universal mathematical assistant systems (MAS) (see Calculemus 2007).

There are various ways in which these two subjects of programming languages and systems for mathematics meet:

  • Many systems for mathematics contain a dedicated programming language. For instance, most computer algebra systems contain a dedicated language (and are frequently built in that same language); some proof assistants (like the Ltac language for Coq) also have an embedded programming language. Note that in many instances this language captures only algorithmic content, and declarative or representational issues are avoided.
  • The mathematical languages of many systems for mathematics are very close to a functional programming language. For instance the language of ACL2 is just Lisp, and the language of Coq is very close to Haskell. But even the mathematical language of the HOL system can be used as a functional programming language that is very close to ML and Haskell. On the other hand, these languages also contain very rich specification capabilities, which are rarely available in most computation-oriented programming languages. And even then, many specification languages ((B, Z, Maude, OBJ3, CASL, etc) can still teach MMSes a trick or two regarding representational power.
  • Conversely, functional programming languages have been getting "more mathematical" all the time. For instance, they seem to have discovered the value of dependent types rather recently. But they are still not quite ready to 'host' mathematics (the non-success of docon being typical). There are some promising languages on the horizon (Epigram, Omega) as well as some hybrid systems (Agda, Focal), although it is unclear if they are truly capable of expressing the full range of ideas present in mathematics.
  • Systems for mathematics are used to prove programs correct. (One method is to generate "correctness conditions" from a program that has been annotated in the style of Hoare logic and then prove those conditions in a proof assistant.) An interesting question is what improvements are needed for this both on the side of the mathematical systems and on the side of the programming languages.
We are interested in all these issues. We hope that a certain synergy will develop between those issues by having them explored in parallel.

These issues have a very colourful history. Many programming language innovations first appeared in either CASes or Proof Assistants, before migrating towards more mainstream languages. One can cite (in no particular order) type inference, dependent types, generics, term-rewriting, first-class types, first-class expressions, first-class modules, code extraction, and so on. However, a number of these innovations were never aggressively pursued by system builders, letting them instead be developped (slowly) by programming language researchers. Some, like type inference and generics have flourished. Others, like first-class types and first-class expressions, are not seemingly being researched by anyone.

We want to critically examine what has worked, and what has not. Why are all the current ``popular'' computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? But also look at question like what forms of polymorphism exists in mathematics? What forms of dependent types exist in mathematics? How can MMS regain the upper hand on issues of 'genericity'? What are the biggest barriers to using a more mainstream language as a host language for a CAS or an ATP?

This workshop will accept two kinds of submissions: full research papers as well as position papers. Research papers should be nore more than 15 pages in length, and positions papers no more than 3 pages. Submission will be through EasyChair. An informal version of the proceedings will be available at the workshop, with a more formal version to appear later. We are looking into having the best papers completed into full papers and published as a special issue of a Journal (details to follow).

Important Dates

April 25, 2007: Submission Deadline
June 29-30, 2007: Workshop

Program Committee

Lennart Augustsson [Credit Suisse]
Wieb Bosma[Radboud University Nijmegen, Netherlands]
Jacques Carette (co-Chair) [McMaster University, Canada]
David Delahaye [CNAM, France]
Jean-Christophe Filliâtre [CNRS and Université de Paris-Sud, France]
John Harrison [Intel Corporation, USA]
Markus (Makarius) Wenzel [Technische Universität München, Germany]
Freek Wiedijk (co-Chair) [Radboud University Nijmegen, Netherlands]
Wolfgang Windsteiger [University of Linz, Austria]

Location and Registration

Location and registration information can be found on the Calculemus web site.

Josh Burdick | 29 Mar 06:05 2007

allowing "almost" a fixpoint?

  I have a question about an idea for adding "almost" a fixpoint to
an otherwise strongly-normalizing language.  I'm going to write CC here
to mean the Calculus of Constructions (without inductive types), but I
think the idea is relevant to Epigram, since it's strongly normalizing.

  CC relies on strong normalization for its soundness, so you
can't just toss an axiom like

fix : forall T. (T -> T) -> T

into the context, because then all types are inhabited, something
like "27 < 4" is trivially provable, and (for instance) any proofs you
use for array bounds are useless.

  However, in CC, Ackerman's function is definable.  I omit the  
definition here (because I don't know it :/), so you should be able to

reallyHugeNumber = ackerman 20 20 : forall  T. (T -> T) -> (T -> T)

  It seems like, at this point, a proof that uses "reallyHugeNumber" is
going to be sound.  But in practical terms, the "zero" arg will never
get called; "reallyHugeNumber" will just call the "successor" arg
a very large number of times.

  In that case, would it be sound to introduce a constant

inf : forall T. (T -> T) -> (T -> T)

which just always calls its "successor" arg infinitely many times?
  It seems like doing so would allow potentially unbounded recursion
without compromising proof soundness, for types which are inhabited.
It's sort of funny-looking, though: to write a factorial function,
for instance, you have to give "inf" an int, which doesn't get used
for anything.

  Still, since Epigram is right between programming languages and proof
checkers, it seemed worth asking: does this make sense?

  (The idea is a lot like

Herman Geuvers, Erik Poll and Jan Zwanenburg. Safe Proof Checking in
Type Theory with Y,  Proceedings of CSL'99, the 13 International
Workshop on Computer Science Logic, Madrid, Spain. Pages 439--452.

  except there, the Y has to be reduced away before the proof is
accepted.  It also seems a bit like the idea of "admissable types" in

  Josh Burdick