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]
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