Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992. ,
DOI : 10.1093/logcom/2.3.297
Tom: Piggybacking Rewriting on Java, Proceedings of RTA, 2007. ,
DOI : 10.1007/978-3-540-73449-9_5
URL : https://hal.archives-ouvertes.fr/inria-00142045
Automated Proof Construction in Type Theory Using Resolution, Journal of Automated Reasoning, vol.29, issue.3-4 1, pp.253-275, 2002. ,
DOI : 10.1007/10721959_10
Normalization in supernatural deduction and in deduction modulo. Available on the author's webpage, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00141720
Superdeduction at Work, 2007. ,
DOI : 10.1007/978-3-540-73147-4_7
URL : https://hal.archives-ouvertes.fr/inria-00141672
Unbounded Proof-Length Speed-Up in Deduction Modulo, 2007. ,
DOI : 10.1007/978-3-540-74915-8_37
URL : https://hal.archives-ouvertes.fr/inria-00138195
The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001. ,
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, Proceedings of TYPES, 2003. ,
DOI : 10.1007/978-3-540-24849-1_10
URL : https://hal.archives-ouvertes.fr/inria-00100113
Embedding PTS in the ??calculus modulo, Proceedings of TLCA, 2007. ,
The duality of computation, Proceedings of ICFP '00, pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
Proof normalization for a first-order formulation of higher-order logic, Proceedings of TPHOL, pp.105-119, 1997. ,
DOI : 10.1007/BFb0028389
URL : https://hal.archives-ouvertes.fr/inria-00073306
Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003. ,
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
Cut elimination for Zermelo's set theory. Available on author's web page ,
Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003. ,
DOI : 10.1007/BFb0037116
Arithmetic as a Theory Modulo ,
DOI : 10.1007/978-3-540-32033-3_31
A Proof-Theoretic Approach to Logic Programming, Journal of Logic and Computation, vol.1, issue.5, pp.635-660, 1991. ,
DOI : 10.1093/logcom/1.5.635
Reconstruction proofs at the assertion level, Proceedings of CADE, pp.738-752, 1994. ,
Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, issue.1-2, pp.91-119, 2000. ,
DOI : 10.1016/S0304-3975(99)00171-1
External rewriting for skeptical proof assistants, Journal of Automated Reasoning, vol.29, issue.3/4, pp.309-336, 2002. ,
DOI : 10.1023/A:1021975117537
URL : https://hal.archives-ouvertes.fr/inria-00101009
Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning, pp.190-201, 1992. ,
Natural Deduction. A Proof-Theoretical Study, Stockholm Studies in Philosophy. Almqvist & Wiksell, vol.3, issue.2, 1965. ,
Certified mathematical hierarchies: the focal system, Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings, 2005. ,
Strong normalisation for a Gentzen-like cutelimination procedure, Proceedings of TLCA, pp.415-430, 2001. ,
Strong Normalisation of Cut-Elimination in Classical Logic, Fundam. Inform, vol.45, issue.4 6, pp.123-155, 2001. ,
DOI : 10.1007/3-540-48959-2_26
The Language ??: Circuits, Computations and Classical Logic, Proceedings of ICTCS'05, pp.81-96, 2005. ,
DOI : 10.1007/11560586_8
A Core Language for Rewriting, Proceedings of WRLA, 1998. ,
DOI : 10.1016/S1571-0661(05)80027-1
Typage et déduction dans le calcul de réécriture, 2002. ,