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 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
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 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
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
Articles de conférence
- Typing coroutines in subtractive logic. In Actes des Journées Francophones sur les Langages Applicatifs, pages 1-19, INRIA, Collection Didactique , 1999. www