- About dokuwiki
The Lots of Logic (LOL) seminar series is a forum for:
The intended audience of these seminars are Ph.D. students, but the seminar is open to all. Students are particularly encouraged to attend and present their work.
The seminar meets on Wednesdays at 14:00. Announcements will be made roughly a week in advance. If you want to attend a talk and have a conflict at the usual time, please speak up and suggest a different time.
Mathieu Boespflug and Chantal Keller, Tuesday, 19 October, 2010
Dowek et al. have proposed in recent years the lambda-Pi-modulo calculus as a universal target framework for other front-end proof languages and environments. One advantage of such a universal format is that a single, small and modular trusted base is all that is required to check proofs from a variety of environments, given translations to lambda-Pi-modulo. But perhaps more interestingly, such a common formalism for proofs opens the door to the integration of collaborative proof efforts from teams in heterogeneous environments.
Dedukti is a type-checker for lambda-Pi-modulo. We focus in this talk on the design decisions behind Dedukti that make it well suited as an implementation of a logical framework. We will illustrate this discussion with specific encodings, namely that of the Calculus of Inductive Constructions with one universe using an extension of Cousineau and Dowek's shallow embedding of all functional PTS into lambda-Pi-modulo, as well as Keller's shallow embedding of HOL.
Superdeduction in Lambda bar mu mu tilde
Clément Houtmann, Wednesday, 29 September 2010
Abstract: Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way.
A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on Christian Urban's work on classical sequent calculus. However the computational content of Christian Urban's calculus is not directly related to the (lambda-calculus based) Curry-Howard correspondence. In contrast the Lambda bar mu mu tilde calculus is a lambda-calculus for classical sequent calculus.
This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the Lambda bar mu mu tilde calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the Lambda bar mu mu tilde calculus.