| Tristan Crolard | Publications | Enseignement |
“Certification de programmes impératifs d'ordre supérieur avec mécanismes de contrôle”. T. Crolard. Mémoire d'Habilitation à Diriger des Recherches. Soutenue le 31 Mars 2010 à l'Université Paris-Est.
Preface to the special issue of Fundamenta Informaticae (Volume 84, Number 2, 2008) dedicated to papers related to the two workshops on “Logic for Pragmatics” WoLP03 and WoLP04. G. Bellin, S. Berardi and T. Crolard.
Excerpt from the call for papers. The project “Logics for Pragmatics”, as presented in the workshops WoLP03, Verona (Italy) and WoLP04, Paris (France), tries to characterize the logical properties of the illocutionary acts of asserting, conjecturing, commanding etc., using the methods of logic (proof theory and model theory) and of category theory. In this perspective, intuitionistic, deontic and causal reasoning are best formalized as intensional logics and their modal translations into classical system with Kripke's semantics are regarded as “reflections” of illocutionary acts into the underlying “propositional content”. To theoretical computer science and computational logic this view has so far offered clear motivations for the study of polarized (“assertive versus conjectural”) systems, of the logic of “causal explanation” and of the interplay between linear Horn logic and the intuitionistic consequence relation. Computational interpretations of classical logic are also to be investigated in this light.
“Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control”. T. Crolard and E. Polonowski. Selected Papers of the 22th Nordic Workshop on Programming Theory (NWPT'10). Journal of Logic and Algebraic Programming. Volume 81, Number 3, 2012, pp 181-208.
Abstract. We derive a Floyd-Hoare logic for non-local jumps and mutable higher-order procedural variables from a formulæ-as-types notion of control for classical logic. A key contribution of this work is the design of an imperative dependent type system for Hoare triples, which corresponds to classical logic, but where the famous consequence rule is admissible. Moreover, we prove that this system is complete for a reasonable notion of validity for Hoare judgments.
“Extending the Loop Language with Higher-Order Procedural Variables”. T. Crolard, E. Polonowski and P. Valarcher. ACM Transactions on Computational Logic. Special Issue on Implicit Computational Complexity. Volume 10, Number 4, 2009, pp 1-37.
Abstract. We extend Meyer and Ritchie's Loop language with
higher-order procedures and procedural variables and we show that
the resulting programming language (called
we define a translation of the
using a converse translation, we show that
Moreover, we define the “iteration rank” of a
“On the expressive power of the
Abstract. We define a translation of Meyer and
Ritchie's
“A formulae-as-types interpretation of Subtractive Logic”. T. Crolard. Journal of Logic and Computation. Special issue on Intuitionistic Modal Logic and Application. Volume 14, Issue 4, August 2004. pp 529-570.
Abstract. We present a formulae-as-types interpretation of Subtractive Logic (i.e. bi-intuitionistic logic). This presentation is two-fold: we first define a very natural restriction of the λμ-calculus which is closed under reduction and whose type system is a constructive restriction of the Classical Natural Deduction. Then we extend this deduction system conservatively to Subtractive Logic. From a computational standpoint, the resulting calculus provides a type system for first-class coroutines (a restricted form of first-class continuations).
“Subtractive logic”. T. Crolard. Theoretical Computer Science 254:1–2(2001):151-185.
Abstract. This paper is the first part of a work whose purpose is to investigate duality in some related frameworks (cartesian closed categories, lambda-calculi, intuitionistic and classical logics) from syntactic, semantical and computational viewpoints. We start with category theory and we show that any bicartesian closed category with coexponents is degenerated (i.e. there is at most one arrow between two objects). The remainder of the paper is devoted to logical issues. We examine the propositional calculus underlying the type system of bicartesian closed categories with coexponents and we show that this calculus corresponds to subtractive logic: a conservative extension of intuitionistic logic with a new connector (subtraction) dual to implication. Eventually, we consider first order subtractive logic and we present an embedding of classical logic into subtractive logic.
“A confluent λ-calculus with a catch/throw mechanism”. T. Crolard. Journal of Functional Programming 9:6(1999):625-647
Abstract. We derive a confluent λ-calculus with a catch/throw mechanism (called λct-calculus) from M. Parigot's λμ-calculus. We also present several translations from one calculus into the other which are morphisms for the reduction. We use them to show that the λct-calculus is a retract of λμ-calculus (these calculi are isomorphic if we consider only convertibility). As a by-product, we obtain the subject reduction property for the λct-calculus, as well as the strong normalization for λct-terms typable in the second order classical natural deduction.
“A Type Theory which is complete for Kreisel's Modified Realizability”. T. Crolard. A Tutorial Workshop on Realizability and Applications'99. Proc. in ENTCS, volume 23, issue 1, pages 58-73. 1999.
Abstract. We define a type theory with a strong elimination rule for existential quantification. As in Martin-Löf's type theory, the “axiom of choice” is thus derivable. Proofs are also annotated by realizers which are simply typed λ-terms. A new rule called “type extraction” which extracts the type of a realizer allows us to derive the so-called “independance of premisses” schema. Consequently, any formula which is realizable in HAω according to Kreisel's modified realizability, is derivable in this type theory.
“WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation.”. S. Varoumas and T. Crolard. Proceedings of the 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019), pages 5:1-5:12, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Stuttgart, Germany, OpenAccess Series in Informatics (OASIcs) 72, 2019.
Abstract. 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.
“A Coq-based synthesis of Scala programs which are correct-by-construction”. Y. Bakouny, T. Crolard and D. Mezher. FTfJP'17: 19th Workshop on Formal Techniques for Java-like Programs Proceedings, June 2017, pp. 2, Barcelona, Spain, (DOI: 10.1145/3103111.3104041).
Abstract. 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.
“A verified abstract machine for functional coroutines”. T. Crolard. Proceedings of the Workshop on Continuations (WoC'15) - Satellite event of ETAPS 2015, June 2016, EPTCS Vol. 212, pp. 1-17, London, UK. (DOI: 10.4204/EPTCS.212.1). The companion technical report and Coq sources files are also available.
Abstract. Functional coroutines are a restricted form of control mechanism, where each continuation comes with its local 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 which is proved to be correct for functional coroutines. Therefore, this abstract machine also provides a direct computational interpretation of the Constant Domain logic.
“Formal Methods for Critical Systems: A verified implementation of nested procedures”. T. Crolard (invited talk). IEEE International Conference on Applied Research in Computer Science and Engineering (ICAR'15), Lebanon, October 2015 (DOI: 10.1109/ARCSE.2015.7338125).
Abstract. This work is part of a broad effort to develop a formal representation of SPARK Ada programs suitable for supporting machine-verified static analyses and translations. In collaboration with SAnToS Labs (Kansas State University) and AdaCore (the GNAT Pro Company), we have previously formalised the dynamic semantics for small subset of the SPARK Ada language, including the encoding of some run-time checks. In this talk, we focus on Ada procedures and, to be more specific, on the semantics of nested and mutually recursive procedures. In particular, we present a proof-of-concept formalisation of an abstract P-machine and we describe some of the meta-theory we have checked with the Coq proof assistant.
“Towards the formalization of spark 2014 semantics with explicit run-time checks using coq” (extended abstract). P. Courtieu, M. V. Aponte, T. Crolard, Z. Zhang, F. Robby, J. Belt, J. Hatcliff, J. Guitton, and T. Jennings. In Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT '13, pp. 21–22, New York, NY, USA, 2013. ACM.
Abstract. We present the first steps of a broad effort to develop a formal representation of SPARK 2014 suitable for supporting machine-verified static analyses and translations. In our initial work, we have developed technology for translating the GNAT compiler's abstract syntax trees into the Coq proof assistant, and we have formalized in Coq the dynamic semantics for a toy subset of the SPARK 2014 language. SPARK 2014 programs must ensure the absence of certain run-time errors (for example, those arising while performing division by zero, accessing non existing array cells, overflow on integer computation). The main novelty in our semantics is the encoding of (a small part of) the run-time checks performed by the compiler to ensure that any well-formed terminating SPARK programs do not lead to erroneous execution. This and other results are mechanically proved using the Coq proof assistant. The modeling of on-the-fly run-time checks within the semantics lays the foundation for future work on mechanical reasoning about SPARK 2014 program correctness (in the particular area of robustness) and for studying the correctness of compiler optimizations concerning run-time checks, among others.
“Monadic reflection in Lax logic” (extended abstract). T. Crolard. Proceedings of the First International Workshop on Theory and Practice of Delimited Continuations (TPDC'11, affiliated with RDP'11). Novi Sad (Serbia) 29-30 May, 2011.
Abstract. We revisit, from a logical standpoint, Filinski's implementation of Moggi's monadic reflection using delimited control operators. We show that monadic reflection can be applied in Lax logic to provide some computational content to various axioms of the form ◊φ⇒φ where ◊ is a representable monad. We also discuss the meaning of this axiom for some standard monads.
The formalization of these results in the Twelf proof assistant, with the corresponding style file, are also available.
“Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control”. T. Crolard and E. Polonowski. Proceedings of the 22th Nordic Workshop on Programming Theory (NWPT'10). Turku (Finland), 10-12 November, 2010. TUCS General Publications, No 57, pp. 70-71. Turku Centre for Computer Science, November 2010.
Abstract. 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.
“On the expressive power of the
Abstract. We define a translation of the
elementary imperative language
“Automatic Parametric Verification of Root Contention Protocol based on Abstract State Machines and First Order Timed Logic”, D. Beauquier, T. Crolard and E. Prokofieva. Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Lecture Notes in Computer Science, volume 2988, pp. 372-387. Springer-Verlag. 2004.
Abstract. The paper presents a verification of the IEEE Root Contention Protocol as an illustration of a new and innovative approach for the verification of real-time distributed systems. Systems are modeled with basic Gurevich abstract state machines (ASMs), and requirements are expressed in a first order timed logic (FOTL). FOTL is undecidable, however the protocol we study is in a decidable class of practical interest. Advantages of this framework are twofold: on the one hand, a great expressive power which permits in particular an easy treatment of parameters, on the other hand the modeling task is simplified by an adequat choice of tools.
“Automatic verification of real time systems: a case study”. D. Beauquier, T. Crolard and E. Prokofieva. Proceedings of the 3rd International Workshop Automated Verification of Critical Systems (AVoCS'03). April 2-3, 2003, Southampton (GB). Technical Report DSSE-TR-2003-2, pp. 1-11. 2003.
Abstract. We propose here a tool which implements an algorithm proposed for a decidable class of verification problems and we illustrate the efficiency of the method by giving an automatic treatment of the well-known benchmark called the Generalized Railroad Crossing Problem. The controller is specified (in all its generality) as a 4-line long Gurevich Abstract State Machines (ASM) which is then automatically translated into a FOTL formula which characterizes its set of runs.
“Impossibility of essential real-time garbage collection in the general case”. D. Beauquier, T. Crolard, A. Durand, and A. Slissenko. In Proc. of the 3nd International Conf. on Computer Science and Information Technologies, September 2001, Yerevan, Armenia, pp. 113-117. National Academy of Sciences of Armenia, 2001.
Abstract. We give an example of a computational problem for which no RAM (random access machine) can ensure a non-trivial garbage collection though a large amount of used memory can be in principle freed starting from some time moment. This example is of theoretical nature and means only that there can be no universal algorithm for “sufficiently good” real-time garbage collection applicable in all situations.
“Typage des coroutines en logique soustractive”. T. Crolard. Journées Francophones des Langages Applicatifs. Février 99. Actes publiés dans la Collection Didactique de l'INRIA, pp. 73-92. 1999.
Résumé. Nous étudions le sens calculatoire de la soustraction, le connecteur dual de l'implication, en exploitant la correspondance de Curry-Howard. En nous appuyant sur la dualité et la Déduction Naturelle Classique de M. Parigot, nous définissons une restriction du λμ-calcul stable par réduction, dont le système de types correspond à la logique soustractive. Dans ce calcul, tout terme typable au second ordre est fortement normalisable. Les objets typés par la soustraction sont interprétés comme des contextes de coroutines de première classe.
“A program logic for higher-order procedural variables and non-local jumps”. T. Crolard and E. Polonowski. Technical Report 4 (2011).
Abstract. 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. We obtain thus an indirect formulas-as-types interpretation of delimited continuations in a dependently-typed framework.
“A Formally Specified Program Logic for Higher-Order Procedural Variables and non-local Jumps”. T. Crolard. Technical Report 5 (2011).
Abstract. 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 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).
“A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables”. T. Crolard and E. Polonowski. Technical Report 3 (2009).
Abstract. We formally specified the type system
and operational semantics of
“Quantifiers are not interdefinable in the second-order propositional constant domain logic”. T. Crolard. Manuscript (2008).
Abstract. We show that the universal quantifier is not definable from the existential quantifier in the second order propositional constant domain logic. To prove this, we exhibit a (full) Kripke model where no closed formula built from ⊤,⊥,∨,∧,→,∃ has the same semantics as the formula ∀X(X∨¬X). This is in contrast to second order propositional subtractive logic where the universal quantifier is definable from the existential quantifier and subtraction.
“A Tool for Automated Verification of Parameterized Timed Algorithms”. T. Crolard and E. Prokofieva. Technical Report 15 (2004).
Abstract. We present a tool developed for automated verification of parameterized real-time systems. Algorithm specification is provided as Timed Gurevich Abstract State Machines while requirements are expressed as formulas of the First Order Timed Logic (FOTL). In our framework, the semantics of an ASM is also defined as a FOTL-formula. Thus any verification problem amounts to proving the validity of some FOTL-formula. Our method is based on a decidable subclass of FOTL which models some “finiteness” properties of control systems.
“A Constructive Restriction of the λμ-calculus”. T. Crolard. Technical Report 02 (2002).
Abstract. We define a very natural restriction of M. Parigot's λμ-calculus which is stable under reduction and whose type system is a restriction of the Classical Natural Deduction to intuitionistic logic. However, we show that this system is in some sense degenerated unless we provide a native disjunction. We prove that the system with native disjunction is conservative over DIS-logic (which is a constructive logic). From a computational standpoint, this restriction on λμ-terms prevents a coroutine from accessing the local environment of another coroutine.
“A predicate logic framework for mechanical verification of real-time Gurevich Abstract State Machines: A case study with PVS.” D. Beauquier, T. Crolard and A. Slissenko. Technical Report 25 (2000).
Abstract. We describe general principles and a tool that permit to get a rather short and clear PVS proof of verification of the Generalized Railroad Crossing Problem. The problem is treated completely following the initial specification practically without any modifications. Such a direct, complete and easy to understand formal treatment of the problem has never been done before. The framework we use is rather general and we believe it can be used for verification of other real-time systems.
“Defining co-inductive types in second-order subtractive logic (and getting a coroutine-based implementation of streams)”. T. Crolard. Deducteam Seminar, November 2012.
Abstract. Subtractive logic is a conservative extension of intuitionistic logic with a new connective, the subtraction, dual to implication. The subtraction is of course definable in classical logic, and as consequence, we can derive the computational content of this connective: we obtain a restricted form of first-class continuations which correspond to coroutines. In this talk, we will focus on the following application: co-inductive types are definable in second-order subtractive logic using an encoding dual the usual encoding of inductive types (from Fortune, Leivant & O'Donnell). Surprisingly, as a special case, we recover the conventional implementation of streams using coroutines (as in Kahn networks).
“A formulae-as-types interpretation of First-Order Subtractive Logic”. T. Crolard. First Workshop on the Logic for Pragmatics. University of Verona (Italy). September 2003.
Abstract. We present a formulae-as-types interpretation of First-Order Subtractive Logic in terms of first-class coroutines. For that purpose, we first define a very natural restriction of the dependently-typed λμ-calculus which is closed under reduction and whose dependent type system corresponds to the Constant Domain Logic. Then we extend this deduction system conservatively to First-Order Subtractive Logic. From a computational standpoint, the resulting calculus provides a dependent type system for first-class coroutines.
“Real-time garbage collection and complexity issues”. T. Crolard and A. Durand. Workshop on Specification and Verification of Real-time Systems. LACL, Université Paris 12. November 2000.
Abstract. In most real-time systems, static scheduling requires a “worst-case execution time” for each process. In this area, the worst-case complexity of an algorithm is thus more relevant than its average complexity. On the other hand, real-time systems developpers naturally wish to benefit from usual features of high-level programming languages, such as garbage collection. In the talk we will discuss some practical and theoretical issues concerning the overhead of a real-time garbage collection.
“Formalisation et vérification du problème du passage à niveau dans Coq et PVS”. Journée spéciale études comparées systèmes de preuves. T. Crolard. INRIA Rocquencourt. Mars 2000.
Résumé. Le problème du « passage à niveau » peut s'énoncer ainsi : un contrôleur doit gérer un passage à niveau pour une route croisant une ou plusieurs voies ferrées. La première contrainte concerne la sûreté : le passage doit être fermé lorsqu'un train passe, la seconde concerne la disponibilité : le passage doit être ouvert le plus souvent possible. Il s'agit d'un exemple type de problème temps-réel, dont une solution a été proposée par D. Beauquier et A. Slissenko. Cette solution s'appuie sur une GASM (Gurevich Abstract State Machine) temporisée pour exprimer l'algorithme et sur une logique temps-réel du premier ordre pour montrer les propriétés souhaitées (sûreté et disponibilité). Nous présenterons une tentative pour traduire la preuve de sûreté dans Coq et la traduction complète de la même preuve dans PVS.
The Tm2elf translator. T. Crolard. October 2011.
Description. Tm2elf is a translator which converts a TeXmacs source file into Twelf syntax. The translator takes advantage of TeXmacs powerful macro system and XML-like native format to provide a user-friendly interface to Twelf combined with a high-quality pretty-printer. The tool, which is developed in ML, is distributed as a command-line application (the source code is available on request). Several examples are also provided, including the slides presented at TPDC'11 [15].
The LoopW translator and proof-checker. T. Crolard and E. Polonowski. June 2009.
Description. The LoopW translator and proof
checker is a tool which checks a dependently-typed imperative
The ASM2FOTL translator. T. Crolard. December 2004.
Description. The ASM2FOTL translator is a tool for translating a Timed ASM (Gurevich Abstract State Machine) into a First Order Timed Logic (FOTL) theory (conforming either to PVS syntax or to Reduce syntax). Some examples of GASM are also provided. The tool, which is developed in ML, is distributed as a command-line application (the source code is available on request). For more information, see Technical Report 25 (2000) above [28].
“Extension de l'isomorphisme de Curry-Howard au traitement des exceptions (application d'une étude de la dualité en logique intuitionniste)”. T. Crolard. Thèse de Doctorat. Décembre 1996. Université Paris 7 - Denis Diderot.
Résumé. Nous proposons un système pour typer le traitement des exceptions dans les langages fonctionnels. Ce systme est obtenu en exploitant l'isomorphisme de Curry-Howard, a partir de la logique intuitionniste (ou classique) étendue par le connecteur dual de l'implication : la soustraction. La dualité a été utilisée, comme outil de construction et de démonstration, dans l'étude de ce connecteur, sous les quatre angles suivants : 1) la théorie des catégories, 2) les sémantiques algébriques, topologiques et de Kripke, 3) la théorie de la démonstration et 4) l'aspect calculatoire. Les résultats principaux sont :
Les catégories bi-cartésiennes fermées
sont nécessairement
dégénérées en présence de
la soustraction et par conséquent la soustraction
n'admet pas d'interprétation dans la catégorie
des ensembles.
La dualité est une notion intuitionniste dans le sens
ou les modèles de Kripke permettent
d'interpréter la soustraction, et de plus
coïncident avec les modèles topologiques de la
soustraction (dits bi-topologiques).
Il existe une traduction très simple de la logique
classique vers la logique intuitionniste soustractive. Cette
traduction s'étend directement aux preuves sans
coupures du calcul des séquents de Gentzen.
La soustraction permet de typer une instruction proche du
“try with” du langage Caml, ceci dans les cadres
classiques et intuitionnistes.
Un dernier résultat, indépendant, concerne la
réalisabilité modifiée.