6 citations · 9 across the 6 of their papers we have counts for
6 papers
A Coq-based synthesis of Scala programs which are correct-by-construction
Youssef El Bakouny, Tristan Crolard, Dani Mezher
The present paper introduces Scala-of-Coq, a new compiler that allows a Coq-based synthesis of Scala programs which are "correct-by-construction". A typical workflow features a use…
A verified abstract machine for functional coroutines
Tristan Crolard
Functional coroutines are a restricted form of control mechanism, where each coroutine is represented with both a continuation and an environment. This restriction was originally o…
Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control
Tristan Crolard, Emmanuel Polonowski
We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formulæ-as-types notion of control for classical logic. The main contribution…
A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps
Tristan Crolard
We formally specified a program logic for higher-order procedural variables and non-local jumps with Ott and Twelf. Moreover, the dependent type systems and the translation are bot…
A program logic for higher-order procedural variables and non-local jumps
Tristan Crolard, Emmanuel Polonowski
Relying on the formulae-as-types paradigm for classical logic, we define a program logic for an imperative language with higher-order procedural variables and non-local jumps. Then…
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Tristan Crolard, Emmanuel Polonowski
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…