A type theory which is complete for Kreisel's modified realizability. - Tristan Crolard (Realizability Semantics and Applications@FLoC, 1999)

A confluent lambda-calculus with a catch/throw mechanism. - Tristan Crolard (J. Funct. Program., 1999)

Subtractive logic. - Tristan Crolard (Theor. Comput. Sci., 2001)

Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. - Danièle Beauquier; Tristan Crolard; Evguenia Prokofieva (TACAS, 2004)

A Formulae-as-Types Interpretation of Subtractive Logic. - Tristan Crolard (J. Log. Comput., 2004)

On the Expressive Power of the Loop Language. - Tristan Crolard; Samuel Lacas; Pierre Valarcher (Nord. J. Comput., 2006)

A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables - Tristan Crolard; Emmanuel Polonowski (CoRR, 2009)

Extending the loop language with higher-order procedural variables. - Tristan Crolard; Emmanuel Polonowski; Pierre Valarcher (ACM Trans. Comput. Log., 2009)

A program logic for higher-order procedural variables and non-local jumps - Tristan Crolard; Emmanuel Polonowski (CoRR, 2011)

A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps - Tristan Crolard (CoRR, 2011)

Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control - Tristan Crolard; Emmanuel Polonowski (CoRR, 2011)

Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control. - Tristan Crolard; Emmanuel Polonowski (J. Log. Algebraic Methods Program., 2012)

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. - Pierre Courtieu; Maria-Virginia Aponte; Tristan Crolard; Zhi Zhang; Robby; Jason Belt; John Hatcliff; Jérôme Guitton; Trevor Jennings (HILT, 2013)

A verified abstract machine for functional coroutines. - Tristan Crolard (WoC, 2015)

A Coq-based synthesis of Scala programs which are correct-by-construction. - Youssef El Bakouny; Tristan Crolard; Dani Mezher (FTfJP@ECOOP, 2017)

WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. - Steven Varoumas; Tristan Crolard (WCET, 2019)