Travelled to:1 × Canada
1 × Denmark
1 × France
1 × Japan
1 × Spain
1 × USA
Collaborated with:∅ V.Komendantsky J.Bertot R.Fraer
Talks about:specif (2) coq (2) eratosthen (1) interpret (1) implement (1) parallel (1) theorem (1) present (1) partial (1) languag (1)
Person: Yves Bertot
DBLP: Bertot:Yves
Contributed to:
2008
2005
2001
1996
1991
1990
1995Wrote 7 papers:
- PPDP-2008-BertotK #coq #fixpoint #recursion #semantics
- Fixed point semantics and partial recursion in Coq (YB, VK), pp. 89–96.
- TLCA-2005-Bertot #induction
- Filters on CoInductive Streams, an Application to Eratosthenes’ Sieve (YB), pp. 102–115.
- CAV-2001-Bertot #formal method #proving #theorem proving #verification
- Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
- CADE-1996-BertotB #named
- CtCoq: A System Presentation (JB, YB), pp. 231–234.
- PLDI-1991-Bertot #debugging #specification
- Occurences in Debugger Specifications (YB), pp. 327–337.
- ESOP-1990-Bertot #implementation #interpreter #parallel
- Implementation of an Interpreter for a Parallel Language in Centaur (YB), pp. 57–69.
- TAPSOFT-1995-BertotF #execution #reasoning #specification
- Reasoning with Executable Specifications (YB, RF), pp. 531–545.