Tristan Crolard

17 papers A 1Journal 11Unranked 5
YearRankTypeTitle / Venue / Authors
2019 — conf
WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation.
WCET
Steven Varoumas, Tristan Crolard
2017 — conf
A Coq-based synthesis of Scala programs which are correct-by-construction.
FTfJP@ECOOP
Youssef El Bakouny, Tristan Crolard, Dani Mezher
2017 J jnl
A Coq-based synthesis of Scala programs which are correct-by-construction.
CoRR
Youssef El Bakouny, Tristan Crolard, Dani Mezher
2015 — conf
A verified abstract machine for functional coroutines.
WoC
Tristan Crolard
2013 — conf
Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq.
HILT
Pierre Courtieu, Maria-Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings
2012 J jnl
Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control.
J. Log. Algebraic Methods Program.
Tristan Crolard, Emmanuel Polonowski
2011 J jnl
A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps
CoRR
Tristan Crolard
2011 J jnl
A program logic for higher-order procedural variables and non-local jumps
CoRR
Tristan Crolard, Emmanuel Polonowski
2011 J jnl
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
CoRR
Tristan Crolard, Emmanuel Polonowski
2009 J jnl
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
CoRR
Tristan Crolard, Emmanuel Polonowski
2009 J jnl
Extending the loop language with higher-order procedural variables.
ACM Trans. Comput. Log.
Tristan Crolard, Emmanuel Polonowski, Pierre Valarcher
2006 J jnl
On the Expressive Power of the Loop Language.
Nord. J. Comput.
Tristan Crolard, Samuel Lacas, Pierre Valarcher
2004 J jnl
A Formulae-as-Types Interpretation of Subtractive Logic.
J. Log. Comput.
Tristan Crolard
2004 A conf
Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic.
TACAS
Danièle Beauquier, Tristan Crolard, Evguenia Prokofieva
2001 J jnl
Subtractive logic.
Theor. Comput. Sci.
Tristan Crolard
1999 J jnl
A confluent lambda-calculus with a catch/throw mechanism.
J. Funct. Program.
Tristan Crolard
1999 — conf
A type theory which is complete for Kreisel's modified realizability.
Realizability Semantics and Applications@FLoC
Tristan Crolard