Tristan Crolard
Professeur des Universités
Team: Systèmes sûrs
Personal website: http://cedric.cnam.fr/sys/crolard
Office: 33.1.9B
2019
Articles de conférence
- 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
- 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
- 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
- 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
- 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
- A program logic for higher-order procedural variables and non-local jumps. Technical Report, , 2011.
2010
Articles de conférence
- 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
- Extending the loop language with higher-order procedural variables. In ACM Transactions on Computational Logic, 10 (4): 1-37, 2009. doi www
Divers
- A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables. , Technical Report of the LACL. www
2008
Divers
- Extending the Loop Language with Higher-Order Procedural Variables. , Technical Report of the LACL. www
2006
Articles de revue
- 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
- On the expressive power of Loop language. In 17th Nordic Workshop on Programming Theory, Copenhaguen, Denmark, 2005. www
2004
Articles de revue
- A formulae-as-types interpretation of Subtractive Logic. In Journal of Logic and Computation, 14:4: 529-570, 2004. www
Articles de conférence
- 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
- 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
Articles de revue
- Subtractive logic. In Theoretical Computer Science, 254:1-2: 151-185, 2001. www
Articles de conférence
- 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
- 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