Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq formalizations of calculi with control operators, continuations etc.

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.



Archive powered by MHonArc 2.6.18.

Top of Page