Fabien Renaud

I'm a postdoc at the LIX lab in the Inria team Parsifal. I'm funded by the ProofCert project and work under the supervision of Dale Miller.
During the year 2013-2014, I'm based in the Programming logic group at Chalmers. While still working on the ProoCert project, I interact with the local team.
Previously, I was "ATER" (temporary research and teaching contract) at the University Paris Diderot where I had my Ph.D. thesis.

You can reach me by

Publications

Journal and conference papers

Z. Chihani, D. Miller and F. Renaud, Foundational Proof Certificates in First-Order Logic
- Proceedings of CADE 2013.
- Download (pdf)
Z. Chihani, D. Miller and F. Renaud, Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract).
- Proceedings of PxTP@CADE 2013.
- Download (pdf)
D. Kesner and F. Renaud, A prismoid framework for languages with resources
- TCS 412(37): 4867-4892, 2011.
- Download (pdf)
D. Kesner and F. Renaud, The Prismoid of Resources
- Proceedings of MFCS 34, LNCS 5734, 2009.
- Download (pdf)

Ph.D. thesis

Ph.D thesis (Dec. 2011) - Explicit resources from the point of view of the rewriting theory - under the supervision of Delia Kesner

Technical reports and unpublished articles

Talks / Workshops without reviewving

Programming Logic Seminar: Some Insights into focusing, Chalmers, Sweden, December 2013
Lix Colloqium: A Semantics for Proof Evidence abstract and slides, Palaiseau, November 2013
Team seminar: News from ProofCert, Minneapolis, USA, February 2013
Collegium Logicum 2012: Structural Proof Theory: News from ProofCert, Palaiseau, November 2012
Promis seminar: News from ProofCert, Montreal, Canada, October 2012
Structural meeting 2: Metaconfluence of λj: dealing with non-deterministic replacements, Innsbruck, Austria, October 2011
16ème Rencontres LAC: Bornes des longueurs de réductions en λ-calcul avec substitutions explicites, Paris, November 2010
Workshop Austria-France: Preservation of Strong Normalization for Higher-Order Rewriting Systems explicited, Innsbruck, Austria, 2009
WPI: The Prismoid of Resources, Paris, September 2009
SPT 08: The cube of resources, Paris, November 2008
Team seminar: Explicit parametric resources for lambda-calculus, UBA, Argentina, August 2008

Softwares

I'm a happy user of the programming languages OCaml and λProlog, and of the proof assistant Coq.

You can find ProofCert developments here
I help from time to time to the Teyjus implementation of λProlog.
A simple formalization of λj in Coq

Previous Teaching (in french) at University Paris Diderot

TP Génie Logiciel Avancé (2011-2012)
TP Programmation fonctionelle avancée (2011-2012)
TP Preuve de programmes (2011-2012)
Cours/TD, Projet programmation (2010-2011)
TD, Types de données et objets (2009-2010)
TP, Introduction aux systèmes d'exploitation (2009-2010)
TP, Informatique fondamentale (2008-2009)
TP, Internet et outils (2007-2008)

Participation in summer schools

DigiCosme School - Program Analysis and Verification, Gif-sur-Yvette, 2013
Oregon Programming Language Summer School, Eugene, 2012
CEA-EDF-INRIA Summer school on the Coq proof assistant - Modelling and verifying algorithms in Coq, Paris, 2010