Tristan Crolard

Professeur des Universités
Équipe : Systèmes sûrs
Bureau : 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. Crolard, T. A formulae-as-types interpretation of Subtractive Logic. In First Workshop on the Logic for Pragmatics, Verona, Italy, 2003. www 
  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 

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

Articles de conférence

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