Thesis

[For03]

J. Forest. Réécriture d'ordre supérieur avec motifs. Thèse de doctorat, Université Paris-Sud, Orsay, France, September 2003. [ .html | .ps.bz2 | .ps.gz | .dvi.bz2 | .dvi.gz | .dvi | .ps | .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. [ .ps.bz2 | .ps.gz ]

International journal

[FK07]

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

International conferences

[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.

[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. [ .ps ]

[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. [ .ps.bz2 | .ps.gz | .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. [ .ps.bz2 | .ps.gz | .pdf ]

Drafts

[For]

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