BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × France
1 × Italy
1 × Korea
1 × United Kingdom
2 × Japan
4 × USA
Collaborated with:
G.Barthe S.Z.Béguelin L.Théry P.Strub J.Hsu B.Barras X.Leroy T.Espitau C.Riba M.Pavlova B.Werner F.Pastawski C.Kunz T.Rezk C.Fournet N.Swamy M.Gaboardi S.Blazy Rémi Hutin V.Laporte D.Pichardie Alix Trieu Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner R.Jhala D.Stefan
Talks about:
probabilist (4) program (4) proof (4) type (4) base (4) cryptograph (3) comput (3) compil (3) certif (3) implement (2)

Person: Benjamin Grégoire

DBLP DBLP: Gr=eacute=goire:Benjamin

Contributed to:

POPL 20142014
SAS 20122012
POPL 20092009
CSL 20082008
IJCAR 20082008
FLOPS 20062006
IJCAR 20062006
SAS 20062006
CSL 20052005
TLCA 20052005
ICFP 20022002
ESOP 20182018
POPL 20172017
POPL 20182018
PLDI 20192019
POPL 20202020

Wrote 16 papers:

POPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification
Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
SAS-2012-BartheGB #encryption #proving
Computer-Aided Cryptographic Proofs (GB, BG, SZB), pp. 1–2.
POPL-2009-BartheGB #certification #encryption #proving
Formal certification of code-based cryptographic proofs (GB, BG, SZB), pp. 90–101.
CSL-2008-BartheGR #termination #type system
Type-Based Termination with Sized Products (GB, BG, CR), pp. 493–507.
IJCAR-2008-BartheGP #java #proving #virtual machine
Preservation of Proof Obligations from Java to the Java Virtual Machine (GB, BG, MP), pp. 83–99.
FLOPS-2006-GregoireTW #approach #type system
A Computational Approach to Pocklington Certificates in Type Theory (BG, LT, BW), pp. 97–113.
IJCAR-2006-GregoireT #composition #functional #library #scalability
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers (BG, LT), pp. 423–437.
SAS-2006-BartheGKR #compilation #optimisation
Certificate Translation for Optimizing Compilers (GB, BG, CK, TR), pp. 301–317.
CSL-2005-BarrasG #calculus #induction #on the
On the Role of Type Decorations in the Calculus of Inductive Constructions (BB, BG), pp. 151–166.
TLCA-2005-BartheGP #polymorphism #termination #type system
Practical Inference for Type-Based Termination in a Polymorphic Setting (GB, BG, FP), pp. 71–85.
ICFP-2002-GregoireL #implementation #reduction
A compiled implementation of strong reduction (BG, XL), pp. 235–246.
ESOP-2018-BartheEGGHS #logic #probability #source code
An Assertion-Based Program Logic for Probabilistic Programs (GB, TE, MG, BG, JH, PYS), pp. 117–144.
POPL-2017-BartheGHS #probability #proving #source code
Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.
POPL-2018-BartheEGHS #probability #proving #source code
Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.
PLDI-2019-CauligiSJBWRGBJ #domain-specific language #named
FaCT: a DSL for timing-sensitive computation (SC, GS, BJ, FB, RSW, JR, BG, GB, RJ, DS), pp. 174–189.
POPL-2020-BartheBGHLPT #c #compilation #verification
Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.
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.