A. Miquel.
Relating classical realizability and negative translation
for existential witness extraction.
Accepté à TLCA'09. 2009.
PDF.
A. Miquel.
Relating classical realizability and negative translation
for existential witness extraction.
Accepté à TLCA'09. 2009.
PDF.
A. Arbiser, A. Miquel, A. Ríos.
The lambda-calculus with constructors:
syntax, confluence and separation.
Accepté à JFP. 2009.
S. Lengrand, A. Miquel.
Classical Fω, orthogonality and symmetric candidates.
Annals of Pure and Applied Logic, 153(1-3).
pp 3-20. 2008.
A. Miquel.
Classical program extraction in the calculus of constructions.
Computer Science and Logic (CSL'07). 2007.
PDF.
S. Lengrand, A. Miquel.
A classical version of system Fω.
In Classical Logic and Computation (CLaC'06),
satellite workshop of the
33rd International Colloquium on
Automata, Languages and Programming (ICALP'06).
2006.
A. Arbiser, A. Miquel, A. Ríos.
A lambda-calculus with constructors.
RTA'06.
PS gzippé,
PDF.
Version longue/Long version:
PS gzippé,
PDF.
ML code:
clam.ml,
G. Dowek, A. Miquel. Cut elimination for Zermelo's set theory.
Version soumise/Submitted version:
PS gzippé,
PDF.
A. Miquel. Lambda-Z: Zermelo's Set Theory as a PTS with 4 Sorts.
In Types for Proofs and Programs (TYPES'04).
Résumé. (Disponible sur demande.)
A. Miquel. A Strongly Normalising Curry-Howard Correspondence for
IZF Set Theory. In Computer Science and Logic (CSL'03).
Vienne (Autriche), 2003.
Résumé,
PS gzippé,
PDF.
A. Miquel, B. Werner. The Not So Simple Proof-Irrelevant Model of
CC. In Types for Proofs and Programs (TYPES'02). 2003.
Résumé,
PS gzippé,
PDF.
A. Miquel, The Implicit Calculus of Constructions. Extending Pure
Type Systems with an Intersection Type Binder and
Subtyping. In Proceedings of the fifth International
Conference on Typed Lambda Calculi and Applications (TLCA'01).
Cracovie (Pologne), 2001.
Résumé,
PS gzippé,
PDF.
A. Miquel, A Model for Impredicative Type Systems with Universes,
Intersection Types and Subtyping. In Proceedings of the 15th Annual
IEEE Symposium on Logic in Computer Science (LICS'00).
Santa-Barbara (Cal., USA), 2000.
Résumé,
PS gzippé,
PDF.
A. Miquel. Un afficheur générique d'arbres à l'aide de la géométrie
hyperbolique. In Actes des onzièmes journées francophones des
langages applicatifs (JFLA'00). Mont Saint-Michel, 2000.
Résumé,
PS gzippé.
A. Miquel.
Extracting reliable witnesses from classical realisers.
Manuscrit.
PDF.
A. Miquel. The experimental effectiveness of mathematical proof.
Manuscrit.
PDF.
A. Miquel. A combinatorial proof of strong normalisation
for the simply typed lambda-calculus.
Manuscrit.
PDF.
G. Dowek, A. Miquel. Relative normalization.
Manuscrit.
PS gzippé,
PDF.
A. Miquel. L'intuitionnisme: où l'on construit une preuve.
In Les chemins de la logique, dossier de
Pour la Science, pp. 30–36. Octobre 2005.
A. Miquel. Le Calcul des Constructions implicite: syntaxe et
sémantique. Thèse de doctorat. Université
Paris 7. Décembre 2001.
Résumé,
PS gzippé,
PDF.
A. Miquel. Arguments implicites dans le Calcul des Constructions:
étude d'un formalisme à la Curry. Mémoire de DEA. Université
Paris 7. 1998.
PS gzippé.