About me

Contact

email
quentin.zoinx.heath##lix.zoinx.polytechnique.fr (remove the zoinxes)
snail mail
Quentin Heath
LIX – UMR 7161
École polytechnique
91128 Palaiseau Cedex
FRANCE
office
LIX, bureau 2059
Bâtiment Alan Turing
1 rue Honoré d'Estienne d'Orves
Campus de l'École polytechnique
91120 Palaiseau
office phone
(+33/0)1 77 57 80 37

Misc

my public PGP key (fingerprint: C582 DEF1 9A2B 3F1F 58CA A811 4395 A6B0 4056 5E01)

Papers

Drafts

A proof theory for model checking
work in progress [pdf]
Induction, cycles and focusing
informal technical report [pdf]

Unpublished

Partially justifying an implementation of tabling in an extension of the propositional Horn fragment of Bedwyr v1.4
informal technical report [pdf]

Paper-less talks

Software

Current

Bedwyr  —  a proof search approach to model checking
model checker implemented as a logic programming proof searcher; closely related to teyjus and abella
weBdyr  —  a web interface for Bedwyr
not yet available
GetArg  —  OCaml alternative to Arg inspired by GNU getopt
merges Arg and Getopt

Adjacent

Abella  —  two-level interactive theorem prover
uses a bedwyr-like logic to reason on specifications written in a teyjus-like language
Teyjus  —  λProlog implementation
modern implementation of a higher-order logic programming language

Past

HippoMail  —  C++ mail-to-XML converter (à la hypermail)
aims to be to hypermail what less is to more