[isabelle] Sigma-calculus in Isabelle/HOL



Dear Florian and Ludovic,

we did quite the same work but with types and in COQ
(confluence+subject reduction). we use an HOAS for binders.

The (huge) work is in an 2004 inria tech rep but the final
revised version will be published in JAR this year ...

You may get a local copy on:

http://www-sop.inria.fr/mascotte/Luigi.Liquori/PAPERS/jar-07.pdf

Or you may have a look on the Alberto Ph.D. dissertation thesis
on his web page (together with coq sources)

All the best,

Alberto, Luigi and Marino.


> Subject: [isabelle] Sigma-calculus in Isabelle/HOL
> Date: Fri, 19 Jan 2007 15:54:44 +0100
> From: Florian Kammueller <flokam at cs.tu-berlin.de>
> To: isabelle-users at cl.cam.ac.uk
>
> Hello,
>
> I'd like to announce recent work with Ludovic Henrio on the
> formalization of
> Abadi's and Cardelli's Theory of Objects in Isabelle/HOL. We  formalized
> the untyped
> sigma calculus and proved confluence.
>
> A Technical report is available here https://hal.inria.fr/ inria-00121816 .
> We would appreciate comments and experience reports from people who  have
> performed
> similar experiments.
>
> Florian Kammueller
> --
> Dr. Florian Kammüller, wissenschaftlicher Assistent
> Institut für Softwaretechnik und Theoretische Informatik
> TU-Berlin, Franklinstr 28/29, 10587 Berlin
> Tel +49-30-314 24330



--
 Luigi Liquori, Ph.D,
 INRIA Researcher, Sophia Antipolis
 Project Team Mascotte
 Vox  : +33 4 92 38 71 93
 Fax  : +33 4 92 38 79 71
 Hom  : +33 4 93 67 09 72
 MobFr: +33 6 65 39 51 32
 MobIt: +39 3 49 16 56 45 1
 Off  : Lagrange LS28
 Url  : www-sop.inria.fr/mascotte/Luigi.Liquori
 Eml  : Let (*,#)=(.,@) in Luigi*Liquori#inria*fr
 Pst  : INRIA, 2004 Route des Lucioles - BP 93
        FR-06902 Sophia Antipolis, France





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.