Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sigma-calculus in Isabelle/HOL

Email Gateway (Aug 18 2022 at 10:05):

From: Florian Kammueller <flokam@cs.tu-berlin.de>
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

Email Gateway (Aug 18 2022 at 10:06):

From: Luigi Liquori <Luigi.Liquori@sophia.inria.fr>
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@cs.tu-berlin.de>
To: isabelle-users@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

Last updated: Nov 21 2024 at 12:39 UTC