Travelled to:1 × Serbia
1 × Spain
1 × USA
2 × France
Collaborated with:∅ E.Contejean J.Forest O.Pons X.Urbain M.Aponte Y.Moy M.Sango A.Paskevich T.Crolard Z.Zhang Robby J.Belt J.Hatcliff J.Guitton T.Jennings
Talks about:certifi (2) proof (2) autom (2) explicit (1) composit (1) approach (1) pattern (1) toward (1) termin (1) semant (1)
Person: Pierre Courtieu
DBLP: Courtieu:Pierre
Contributed to:
2013
2012
2011
2010
2001Wrote 5 papers:
- HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using
- Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
- FM-2012-AponteCMS #composition #invariant
- Maximal and Compositional Pattern-Based Loop Invariants (MVA, PC, YM, MS), pp. 37–51.
- RTA-2011-ContejeanCFPU #automation #proving
- Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.
- PEPM-2010-ContejeanPUCPF #approach #automation #proving #termination
- A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
- CSL-2001-Courtieu #normalisation
- Normalized Types (PC), pp. 554–569.