BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Bertot:Yves

Contributed to:

PPDP 20082008
TLCA 20052005
CAV 20012001
CADE 19961996
PLDI 19911991
ESOP 19901990

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.