Tristan Crolard

Professeur des Universités
Office: 33.1.9B

Publications

2019

Articles de conférence

  1. Varoumas, S. and Crolard, T. WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. In 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. doi  www 

2017

Articles de conférence

  1. El Bakouny, Y.; Crolard, T. and Mezher, D. A Coq-based synthesis of Scala programs which are correct-by-construction. In Formal Techniques for Java-like Programs (FTfJP) 2017, Barcelona, Spain, 2017. doi  www 

2016

Articles de revue

  1. Crolard, T. A verified abstract machine for functional coroutines. In Electronic Proceedings in Theoretical Computer Science, 212: 1-17, 2016. doi  www 

2013

Articles de conférence

  1. Courtieu, P.; Aponte, M-V.; Crolard, T.; Zhang, Z.; ,; Belt, J.; Hatcliff, J.; Guitton, J. and Jennings, T. Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq. In High Integrity Language Technology - ACM SIGAda?s Annual International Conference, pages 2, X, Australia, ACM Digital Library , 2013. www 

2012

Articles de revue

  1. Crolard, T. and Polonowski, E. Deriving a Floyd-Hoare logic for non-local jumps from a formulae-as-types notion of control. In Journal of Logic and Algebraic Programming: 181-208, 2012. www 

2011

Rapports

  1. Crolard, T. and Polonowski, E. A program logic for higher-order procedural variables and non-local jumps. Technical Report, , 2011.

2010

Articles de conférence

  1. Crolard, T. and Polonowski, E. Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control. In The 22nd Nordic Workshop on Programming Theory, pages 70-71, Turku Centre for Computer Science, Turku, Finland, TUCS General Publication , 2010. www 

2009

Articles de revue

  1. Crolard, T.; Polonowski, E. and Valarcher, P. Extending the loop language with higher-order procedural variables. In ACM Transactions on Computational Logic, 10 (4): 1-37, 2009. doi  www 

Divers

  1. Crolard, T. and Polonowski, E. A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables. , Technical Report of the LACL. www 

2008

Divers

  1. Crolard, T.; Polonowski, E. and Valarcher, P. Extending the Loop Language with Higher-Order Procedural Variables. , Technical Report of the LACL. www 

2006

Articles de revue

  1. Crolard, T.; Lacas, S. and Valarcher, P. On the Expressive Power of the Loop Language. In Nordic Journal of Computing, 13: http://www.cs.helsinki.fi/njc, 2006. www 

2005

Articles de conférence

  1. Crolard, T.; Lacas, S. and Valarcher, P. On the expressive power of Loop language. In 17th Nordic Workshop on Programming Theory, Copenhaguen, Denmark, 2005. www 

2004

Articles de revue

  1. Crolard, T. A formulae-as-types interpretation of Subtractive Logic. In Journal of Logic and Computation, 14:4: 529-570, 2004. www 

Articles de conférence

  1. Beauquier, D.; Crolard, T. and Prokofieva, E. Automatic Parametric Verification of Root Contention Protocol based on Abstract State Machines and First Order Timed Logic. In TACAS, pages 372-387, Springer-Verlag, France, LNCS 2988 , 2004. www 

2003

Articles de conférence

  1. Beauquier, D.; Crolard, T. and Prokofieva, E. Automatic verification of real time systems: a case study. In Proceedings of the 3rd Automated Verification of Critical Systems (AVoCS'03), pages 1-11, Southampton, United Kingdom, 2003. www 
  1. Crolard, T. A formulae-as-types interpretation of Subtractive Logic. In First Workshop on the Logic for Pragmatics, Verona, Italy, 2003. www 

2001

Articles de revue

  1. Crolard, T. Subtractive logic. In Theoretical Computer Science, 254:1-2: 151-185, 2001. www 

Articles de conférence

  1. Beauquier, D.; Crolard, T.; Durand, A. and Slissenko, A. Impossibility of essential real-time garbage collection in the general case. In Proceedings of the 3nd International Conferences on Computer Science and Information Technologies, pages 113-117, Yerevan, Armenia, 2001. www 

1999

Articles de revue

  1. Crolard, T. A confluent lambda-calculus with a catch/throw mechanism. In Journal of Functional Programming, 9:6: 625-647, 1999. www 
  1. Crolard, T. A Type Theory which is complete for Kreisel's Modified Realizability. In Electronic Notes in Theoretical Computer Science, 23: 1-16, 1999. www 

Articles de conférence

  1. Crolard, T. Typing coroutines in subtractive logic. www 
Top