Ceci est une formalisation d'une partie de ma thèse qui concerne un système
alternatif de calcul des séquents pour les PTS.
This is a formalization of a part of my phd dissertation that shows an
alternative sequent calculus presentation for PTS.
Coq files
tar file: Tested with the
trunk version of Coq (July 2010).
Almost compatible with v8.2 with a minor syntactic
changes when using destruct.
Please modify the Makefile to point
out where coqc is located.
(Based on
Stephane Lengrand's Phd Thesis )
Ceci est une réécriture de la formalisation des PTS classiques ainsi qu'une
formalisation d'une version "Calcul des Sequents" de PTS, avec la preuve que
les deux systemes sont equivalents.
Les preuves d'equivalences sont tirees de la these de Stephane Lengrand (merci
pour les conseils).
This is a rewriting of the old PTS formalization, with a new one which is a
"Sequent Calculus" PTS, along with the proof that those systems are
equivalent.
The equivalence proofs are adaptation of Stephane Lengrand's
Thesis (Thank you for the advices).
Coq files
tar file: Tested with the trunk
version of Coq (July 2010), not yet with 8.2.
Please modify the Makefile to point out
where coqc is located.
Vous trouverez ici une preuve que la Beta/Eta conversion est confluente sur
des termes sans information de type sur les lambdas.
You'll find here a proof that Beta/Eta conversion is confluent over untyped
terms (lambdas without type information).
Coq files
Many thanks to Bruno Barras and Herman Geuvers for their advices
References:
Les preuves sont assez longues au final parce que je n'utilise que tres peu les mecanismes automatiques de coq. Depuis j'ai appris un peu plus sur ce sujet et je pourrais surement les raccourcir et les rendre un poil plus lisible.
Tour du paysage :
PTS.v : la definition bete et mechante des termes + les fonctions de manipulation de DeBruijn
PTS_env.v : definitions de tout ce qui touche aux contextes de typages (lift , insertion, substitution)
PTS_beta.v : definition de beta, de sa cloture transitive et de sa cloture refl / trans / sym (idem pour beta //)
plein de fonctions pour les manipuler et une preuve de la confluence de beta (formalisation de celle de Taits par reduction parallele)
PTS_correctness.v : definition du typage et des lemmes d'inversion (si T type a alors T doit avoir une certaine forme)
principalement des trucs piqués chez bruno remis aux gouts du jour
PTS_subjectred.v : la preuve que ce PTS a la propriete de subject reduction
Le jugement de typage n'est pas forcement tres parlant au debut, mais il a été fait dans l'idée de faciliter la formalisation sur machine.
Une version plus jolie (et avec Eta) est pour bientot.
Back to main page.
Last modified Jun 28 2010