coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Coq formalizations of calculi with control operators, continuations etc.
Chronological Thread
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Coq formalizations of calculi with control operators, continuations etc.
- Date: Wed, 24 Feb 2016 11:41:23 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f170.google.com
- Ironport-phdr: 9a23:GtNYFR1iH5zjTn0ksmDT+DRfVm0co7zxezQtwd8ZsegRLfad9pjvdHbS+e9qxAeQG96LtLQZ26GG7+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZnnnLDus7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOL/R6o1VDDq1KxrRQXlkm9TODcz6mDajoprh6JWuh+7jxN6yo/QJoqSMawtLevmYdoGSD8ZDY5qXCtbD9b5NtNXAg==
Piotr Polesiuk has a formalization of the simply-typed lambda-calculus
with shift0 and reset0, with a logical relation for equivalence, at
http://www.ii.uni.wroc.pl/~ppolesiuk/lrcoherence/
which accompanies the following article
Logical Relations for Coherence of Effect Subtyping
Dariusz Biernacki and Piotr Polesiuk, 2015
http://www.ii.uni.wroc.pl/~dabi/publications/TLCA15/biernacki-polesiuk-TLCA15.pdf
Danko Ilik has worked on "Kripke-CPS" model of intuitionistic and
classical logic, and does a very thorough formalization work alongside
his research. See
http://www.lix.polytechnique.fr/~danko/formal.html
and in particular the formalization of
Constructive completeness of first-order classical and
intuitionistic predicate logic
with respect to Kripke-CPS models
Danko Ilik, 2009
( publications: http://arxiv.org/abs/0904.0071 and
http://arxiv.org/abs/1102.1061 )
which contains a formalization of a mu-mutilda term syntax for
classical sequent calculus, and
Type-directed partial evaluation for level-1 shift and reset in Coq,
Danko Ilik, 2011
( publication : http://arxiv.org/abs/1210.2094 )
On Wed, Feb 24, 2016 at 10:55 AM, Tadeusz Litak
<tadeusz.litak AT gmail.com>
wrote:
> Dear all,
>
> I have a question about $SUBJECT$.
>
> I have a hard time trying to find out whether there are some "canonical" Coq
> formalizations of, let's say, Parigot's \lambda\mu-calculus or related
> formalisms and their basic metatheory.
>
> In particular, I always thought that formalization of, e.g, normalization
> proofs which go via the CPS route would make a nice student project. I have
> a student right now willing to spend some time on this. But I would like to
> avoid reinventing the wheel, and I had the suspicion that there may be more
> than a few formalization efforts already available. Still, casual search
> does not produce all that much. Such calculi do not seem covered, for
> example, by what I can find in the Iron Lambda repository. Am I missing some
> obvious references?
>
>
> Best regards,
> t.
- [Coq-Club] Coq formalizations of calculi with control operators, continuations etc., Tadeusz Litak, 02/24/2016
- Re: [Coq-Club] Coq formalizations of calculi with control operators, continuations etc., Gabriel Scherer, 02/24/2016
Archive powered by MHonArc 2.6.18.