Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o /| /| __ __ __ __ _ _
/ ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __)
(___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/
I N R I A - Rocquencourt
Amphi Turing du bâtiment 1
Lundi 13 mai, 10h30
----------------
Guillaume Claret
----------------
Université Paris 7
=============================================================
Lightweight proof by reflection using a posteriori simulation
of effectful computation
=============================================================
Proof-by-reflection is a well-established technique that employs decision
procedures to reduce the size of proof-terms. Currently, decision procedures
can be written either in Type Theory---in a purely functional way that also
ensures termination---or in an effectful programming language, where they are
used as oracles for the certified checker. The first option offers strong
correctness guarantees, while the second one permits more efficient
implementations.
We propose a novel technique for proof-by-reflection that marries, in Type
Theory, an effectful language with (partial) proofs of correctness. The key to
our approach is to use simulable monads, where a monad is simulable if, for
all terminating reduction sequences in its equivalent effectful computational
model, there exists a witness from which the same reduction may be simulated a
posteriori by the monad. We encode several examples using simulable monads and
demonstrate the advantages of the technique over previous approaches.