arXiv subjects

Tristan Crolard

Publications and source records attributed to Tristan Crolard.

6 recordsLinked to original sources

arXiv2017

A Coq-based synthesis of Scala programs which are correct-by-construction

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 user implementing a Coq functional program, proving this program's correctness with regards to its specification and making use of Scala-of-Coq to synthesize a Scala program that can seamlessly be integrated into an existing industrial Scala or Java application.

cs.PL↗

arXiv2016

A verified abstract machine for functional coroutines

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 obtained by considering a constructive version of Parigot's classical natural deduction which is sound and complete for the Constant Domain logic. In this article, we present a refinement of de Groote's abstract machine for functional coroutines and we prove its correctness. Therefore, this abstract machine also provides a direct computational interpretation of the Constant Domain logic.

cs.LO↗

arXiv2011

Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control

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 of this work is the design of an imperative dependent type system for non-local jumps which corresponds to classical logic but where the famous consequence rule is still derivable.

cs.LO↗

arXiv2011

A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps

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 both executable specifications thanks to Twelf's logic programming engine. In particular, relying on Filinski's encoding of shift/reset using callcc/throw and a global meta-continuation (simulated in state passing style), we have mechanically checked the correctness of a few examples (all source files are available on request).

cs.LO↗

arXiv2011

A program logic for higher-order procedural variables and non-local jumps

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, we show how to derive a sound program logic for this programming language. As a by-product, we obtain a non-dependent type system which is more permissive than what is usually found in statically typed imperative languages. As a generic example, we encode imperative versions of delimited continuations operators shift and reset.

cs.LO↗

arXiv2009

A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables

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 been tested using Isabelle/HOL program extraction facility for inductively defined relations. In particular, the program that computes the Ackermann function type checks and behaves as expected. The main difference (apart from the choice of an Ada-like concrete syntax) with LOOPw comes from the treatment of parameter passing. Indeed, since Ott does not currently fully support alpha-conversion, we rephrased the operational semantics with explicit aliasing in order to implement the out parameter passing mode.

cs.LO↗