Tristan Crolard
Professor
Team: Systèmes sûrs
Personal website: http://cedric.cnam.fr/sys/crolard
Office: 33.1.9B
2019
Conference Articles
- WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. In OpenAccess Series in Informatics (OASIcs), pages 5:1-5:12, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Stuttgart, Germany, OpenAccess Series in Informatics (OASIcs) 72, 2019. doi www
2017
Conference Articles
- A Coq-based synthesis of Scala programs which are correct-by-construction. In FTFJP'17, Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs, Barcelona, Spain, 2017. doi www
2016
Journal Articles
- A verified abstract machine for functional coroutines. In Electronic Proceedings in Theoretical Computer Science, 212: 1-17, 2016. doi www
2013
Conference Articles
- Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq. In ACM Digital Library, pages 2, X, Australia, ACM Digital Library , 2013. www
2012
Journal Articles
- 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
Reports
- A program logic for higher-order procedural variables and non-local jumps. Technical Report, , 2011.
2010
Conference Articles
- Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control. In Proceedings of the 22nd Nordic Workshop on Programming Theory, pages 70-71, Turku Centre for Computer Science, Turku, Finland, TUCS General Publication , 2010. www
2009
Journal Articles
- Extending the loop language with higher-order procedural variables. In ACM Transactions on Computational Logic, 10 (4): 1-37, 2009. doi www
Miscellaneous
- A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables. , Technical Report of the LACL. www
2008
Miscellaneous
- Extending the Loop Language with Higher-Order Procedural Variables. , Technical Report of the LACL. www
2006
Journal Articles
- On the Expressive Power of the Loop Language. In Nordic Journal of Computing, 13: http://www.cs.helsinki.fi/njc, 2006. www
2005
Conference Articles
- On the expressive power of Loop language. In 17th Nordic Workshop on Programming Theory, Copenhaguen, Denmark, 2005. www
2004
Journal Articles
- A formulae-as-types interpretation of Subtractive Logic. In Journal of Logic and Computation, 14:4: 529-570, 2004. www
Conference Articles
- Automatic Parametric Verification of Root Contention Protocol based on Abstract State Machines and First Order Timed Logic. In Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), pages 372-387, Springer-Verlag, France, LNCS 2988 , 2004. www
2003
Conference Articles
- A formulae-as-types interpretation of Subtractive Logic. In First Workshop on the Logic for Pragmatics, Verona, Italy, 2003. www
- 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
Journal Articles
- Subtractive logic. In Theoretical Computer Science, 254:1-2: 151-185, 2001. www
Conference Articles
- 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
Journal Articles
- A Type Theory which is complete for Kreisel's Modified Realizability. In Electronic Notes in Theoretical Computer Science, 23: 1-16, 1999. www
- A confluent lambda-calculus with a catch/throw mechanism. In Journal of Functional Programming, 9:6: 625-647, 1999. www
Conference Articles
- Typing coroutines in subtractive logic. In Actes des Journées Francophones sur les Langages Applicatifs, pages 1-19, INRIA, Collection Didactique , 1999. www