Publications

  • A Rocq Prover STL Formalization with Transformations for Mission Planning
    Danil Berrah; François Pessaux; Alexandre Chapoutot
    Journal of Automated Reasoning, 2026. DOI 10.1007/s10817-026-09763-y, Springer Nature SharedIt link
  • A Proof-Assisted Conversion of Signal Temporal Logic Formulas into Negative Normal Form
    Berrah, D., Pessaux, F., & Chapoutot, A.
    Extended Abstract and Poster, 2025. Available at https://hal.science/hal-05133722
  • Interval-Based Simulation of Zélus IVPs using DynIbex
    Jason Brown, François Pessaux.
    Acta Cybernetica, Special issue for SWIM2019, published 2020/08/19. DOI 10.14232/actacyb.285246
  • Termination Proofs for Recursive Functions in FoCaLiZe
    Catherine Dubois, François Pessaux
  • International Symposium on Trends in Functional Programming 2015.  DOI 10.1007/978-3-319-39110-6_8
  • FoCaLiZe: Inside an F-IDE
    François Pessaux
    1st Workshop on Formal Integrated Development Environment (F-IDE 2014), Satellite workshop of ETAPS 2014, Electronic Proceedings in Theoretical in Computer Science 149, pp 64-78. 2014.
  • Another Tutorial for FoCaLiZe: Playing with Proofs
    Part of the distribution of the FoCaLiZe environment. January 2013.
  • ML Dependency Analysis for Assessors
    Philippe Ayrault, Vincent Benayoun, Catherine Dubois and François Pessaux
    SEFM 2012 - Thessaloniki (Greece), October 2012.
  • Interprétation quantique du logiciel:*)
    2011.
    Published nowhere. Parody of scientific article mixing software and physics. Doesn't intend to be serious...
  • Development Life-cycle of Critical Software Under FoCaL
    Philippe Ayrault, Thérèse Hardin and François Pessaux
    In 2nd International Workshop on Harnessing Theories for Tool Support in Software, TTSS'08, Istambul, 2008.
    Electron. Notes Theor. Comput. Sci., vol. 243, jul 2009, pp. 15-31.
  • Development of a generic voter under FoCaL
    Philippe Ayrault, Thérèse Hardin and François Pessaux.
    In TAP2009 - Zurich, July 2009.
  • The FoCaLiZe Reference Manual 2009-2013.
    Thérèse Hardin, François Pessaux, Damien Doligez, Pierre Weis
    Part of the distribution of the FoCaLiZe environment.
  • Trusted Software within FoCaL
    P. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, T. Hardin, M. Jaume, C. Morisset, F. Pessaux, R. Rioboo, P. Weis.
    In C&ESAR 2008 - Trusting Trusted Computing ? - Rennes (France) , December 2008. 
  • Development life cycle of critical software under FoCal.
    Philippe Ayrault, Thérèse Hardin, François Pessaux
    In 2nd International Workshop on Harnessing Theories for Tool Support in TTSS'08 – Istambul (Turquie) August 2008.
  • PhD report: Détection statique d'exceptions non rattrapées en Objective Caml
    (Sumary only).
  • Type-based analysis of uncaught exceptions (journal version)
    Xavier Leroy, François Pessaux.
    To be published in ACM Transactions on Programming Languages and Systems, 2000.
  • Type-based analysis of uncaught exceptions.
    Xavier Leroy, François Pessaux
    Published in POPL '99. (Available as Postscript letter, Postscript A4, and PDF.) Extended version with detailed proves available as a technical report INRIA.
  • OCamlDoom: ML for 3D action games
    Workshop ML, September 1998, Baltimore (Maryland USA).
  • Ajout d'une conditionnelle dans un système de modules à la Caml  (Adding a conditional construct in a Caml-like module system).
    Journées Francophones des Langages Applicatifs, Janvier 1997, Dolomieux (Isère - FRANCE).
    •
    08/2020