Thesis

[For03]

J. Forest. Réécriture d'ordre supérieur avec motifs. Thèse de doctorat, Université Paris-Sud, Orsay, France, September 2003. [ .html | .pdf ]

[For99]

J. Forest. Définition des stratégies paresseuse et stricte pour TPC et TPC_es. Rapport de DEA, Université Paris-Sud, Orsay, France, 1999.

International journal

[FK07]

J. Forest and D. Kesner. Expression reduction systems with patterns. Journal of Automated Reasoning, 39:513--541, 2007. [ .pdf ]

International conferences

[BCFC11]

A.-G. Bosser, P. Courtieu, J. Forest, and M. Cavazza. Structural analysis of narratives with the coq proof assistant. In M. V. Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, editors, Second conference on Interactive Theorem Proving (ITP 11), volume 6898 of LNCS, Nijmegen, The Netherlands, 2011. Springer.

[CCF⁺11]

E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain. Automated Certified Proofs with CiME3. In M. Schimdt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 10), volume 10 of LIPIcs, pages 21--30, Novi Sad, Serbia, 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ .pdf ]

[CCF⁺10]

E. Contejean, P. Courtieu, J. Forest, A. Paskevich, O. Pons, and X. Urbain. A3pat, an approach for certified automated termination proofs. In Proceedings of PEPM'10, pages 63--72, Madrid, Spain, 2010. ACM. [ .pdf ]

[CFU08]

P. Courtieu, J. Forest, and X. Urbain. Certifying a termination criterion based on graphs, without graphs. In C. Munoz and O. A. Mohamed, editors, Proceedings of TPHOLs'08, volume 5170 of Lecture Notes in Computer Science, pages 183--198, Montréal, Canada, August 2008. Springer-Verlag. [ .pdf ]

[CCF⁺07]

E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain. Certification of automated termination proofs. In B. Konev and F. Wolter, editors, Proceedings of FROCOS'07, volume 4720 of LNAI, pages 148--162, Liverpool, U.K., September 2007. Springer-Verlag. [ .pdf ]

[BFPR06]

G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: a practical tool for the coq proof assistant. In M. Hagiya and P. Wadler, editors, Proceedings of FLOPS'06, volume 3945 of LNCS, pages 114--129. Springer-Verlag, 2006. [ .ps.gz | .pdf ]

[FK03]

J. Forest and D. Kesner. Expression reduction systems with patterns. In R. Nieuwenhuis, editor, 14th International Conference on Rewriting Techniques and Applications, volume 2706 of LNCS, pages 107--122, Valencia, Spain, June 2003. Springer-Verlag. [ .pdf ]

[For02]

J. Forest. A weak calculus with explicit operators for pattern matching and substitution. In S. Tison, editor, 13th International Conference on Rewriting Techniques and Applications, volume 2378 of LNCS, pages 174--191, Copenhagen, Denmark, July 2002. Springer-Verlag. [ .pdf ]

Research and technical reports

[CFU08a]

E. Contejean, J. Forest, and X. Urbain. Deep-embedded unification. Technical Report 1547, CNAM, 2008.

[CCF⁺07b]

E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain. Certification of automated termination proofs. Technical Report 1185, CNAM, 2007. [ .pdf ]

[FL05]

J. Forest and S. Lucas. Proving termination of higher-order functional programs. Technical report, DSIC, Universidad Politécnica de Valencia, Spain, 2005. [ .pdf ]

[For02b]

J. Forest. A weak calculus with explicit operators for pattern matching and substitution. Research Report 1313, LRI, May 2002. [ .pdf ]

Drafts

[For02a]

J. Forest. A proof of strong normalization by reducibility modulo for λ_σw. Unpublished draft, 2002. [ .ps.bz2 | .ps.gz | .ps | .pdf ]