Publications

HAL  arXiv  CSB  DBLP  GoogleScholar  CiteSeer

Submitted

• A size-based termination criterion for dependently-typed higher-order rule-based programs. Journal version of RTA'04 and CSL'05.

2011

• First steps towards the certification of an ARM simulator. With J.-F. Monin, X. Shi and F. Tuong. CPP'11. [HAL]
• Argument filterings and usable rules in higher-order rewrite systems. With K. Kusakari and S. Suzuki. IPSJ Transactions on Programming 4(2), p. 1-12. [HAL]
• Designing a CPU model: from a pseudo-formal document to fast code. With C. Helmstetter, V. Joloboff, J.-F. Monin and X. Shi. RAPIDO'11. Best paper award. [HAL]
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. With A. Koprowski. MSCS 21(4), p. 827-859 © Cambridge University Press. [HAL]

2010

• SimSoC-Cert: a certified simulator for systems on chip. With C. Helmstetter, V. Joloboff, J.-F. Monin and X. Shi. Draft.
• On the confluence of lambda-calculus with conditional rewriting. With C. Riba and C. Kirchner. Journal version of FOSSACS'06. TCS 411(37), p. 3301-3327 © Elsevier Science. [HAL]
• Argument filterings and usable rules in higher-order rewrite systems. With K. Kusakari and S. Suzuki. IEICE Technical Report SS2010-24, Vol. 110, No. 169. [HAL]

2009

• Static dependency pair method based on strong computability for higher-order rewrite systems. With Y. Isogai, K. Kusakari and M. Sakai. IEICE Transactions on Information and Systems E92-D(10), p. 2007-2015. [HAL]
• On the relation between sized-types based termination and semantic labelling. With C. Roux. CSL'09. Acceptance rate: 34/89 = 38%. LNCS 5771 © Springer Verlag. Full version in [HAL].
• Automated verification of termination certificates. With A. Koprowski. INRIA Research Report 6949. [HAL]

2008

• The computability path ordering: the end of a quest. With J.-P. Jouannaud and A. Rubio. CSL'08. Invited paper. LNCS 5213 © Springer Verlag. [HAL]
• From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures. With J.-P. Jouannaud and P.-Y. Strub. TCS'08. Acceptance rate: 16/45 = 36%. IFIP 273 © Springer Verlag. [HAL]

2007

• HORPO with computability closure : a reconstruction. With J.-P. Jouannaud and A. Rubio. LPAR'07. Acceptance rate: 36/78 = 46%. LNCS 4790 © Springer Verlag. [HAL]
• Building decision procedures in the Calculus of Inductive Constructions. With J.-P. Jouannaud and P.-Y. Strub. CSL'07. Acceptance rate: 36/116 = 31%. LNCS 4646 © Springer Verlag. [HAL]
• Computability closure: ten years later. Essay in Honour of Jean-Pierre Jouannaud's 60 Birthday. LNCS 4600 © Springer Verlag. [HAL]
• Automated certification of termination proofs. TYPES'07. Invited talk.
• On the implementation of construction functions for non-free concrete data types. With T. Hardin and P. Weis. ESOP'07. Acceptance rate: 34/136 = 25%. LNCS 4421 © Springer Verlag. [HAL]

2006

• Higher-order termination: from Kruskal to computability. With J.-P. Jouannaud and A. Rubio. LPAR'06. Invited paper. LNCS 4246 © Springer Verlag. [HAL]
• Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. With C. Riba. LPAR'06. Acceptance rate: 38/96 = 40%. LNCS 4246 © Springer Verlag. [HAL]
• Higher-order dependency pairs. WST'06. Acceptance rate: 15/15= 100%. [HAL]
• CoLoR, a Coq Library on Rewriting and termination. With S. Coupet-Grimal, W. Delobel, S. Hinderer and A. Koprowski. WST'06. Acceptance rate: 15/15= 100%. [HAL]
• (HO)RPO revisited. INRIA Research report 5972. [HAL]
• On the confluence of lambda-calculus with conditional rewriting. With C. Riba and C. Kirchner. FOSSACS'06. Acceptance rate: 28/107 = 26%. LNCS 3921 © Springer Verlag. Full version. [HAL].

2005

• Decidability of type-checking in the Calculus of Algebraic Constructions with Size Annotations. CSL'05. Acceptance rate: 33/108 = 30%. LNCS 3634 © Springer Verlag. Full version. [HAL]
• Inductive types in the Calculus of Algebraic Constructions. Journal version of TLCA'03. Fundamenta Informaticae 65(1-2), p. 61-86 © IOS Press. [HAL]
• Definitions by rewriting in the Calculus of Constructions. MSCS 15(1), p. 37-92 © Cambridge University Press. [HAL]

2004

• A type-based termination criterion for dependently-typed higher-order rewrite systems. RTA'04. Acceptance rate: 19/43 = 44%. LNCS 3091 © Springer Verlag. Full version. [HAL]

2003

• Rewriting modulo in Deduction modulo. RTA'03. Acceptance rate: 26/57 = 46%. LNCS 2706 © Springer Verlag. [HAL]
• Inductive types in the Calculus of Algebraic Constructions. TLCA'03. Acceptance rate: 21/40 = 52%. LNCS 2701 © Springer Verlag. [HAL]
• A short and flexible proof of strong normalization for the Calculus of Algebraic Constructions with curried rewriting. Integrated in the MSCS'05 paper.

2002

• An Isabelle formalization of protocol-independent secrecy with an application to e-commerce. Draft. [HAL]
• Inductive-data-type Systems. With J.-P. Jouannaud and M. Okada. TCS 272, p. 41-68 © Elsevier Science. [HAL]

2001

• Type theory and rewriting. Ph.D. Thesis [HAL]. French version. [HAL]. SPECIF 2001 PhD Award.
• Definitions by rewriting in the Calculus of Constructions. LICS'01 © IEEE Computer Society. Acceptance rate: 36/104 = 35%. Kleene Award for best student paper. [HAL]

2000

• Termination and confluence of higher-order rewrite systems. RTA'00. Acceptance rate: 15/41 = 37%. LNCS 1833 © Springer Verlag. Full version. [HAL]

1999

• The Calculus of Algebraic Constructions. With J.-P. Jouannaud and M. Okada. RTA'99. Acceptance rate: 23/46 = 50%. LNCS 1631 © Springer Verlag. Full version. [HAL]

1998

• The Calculus of Algebraic and Inductive Constructions. Master thesis.

1997

• A document-centered approach for an open CASE environment framework connected with the WWW. SEN 22(2) © ACM Press.

Last updated on 9 January 2012. Come back to main page.