[isabelle] Sigma-calculus in Isabelle/HOL
Are you aware of all the recent developments in the nominal
We already provide a usable infrastructure to reason with
named alpha-equated lambda-terms - i.e. we can already reason
about alpha-equivalence classes relatively easily without having
to represent them with de-Bruijn indices. The nominal package
is still a research project, as you write. However, we come already
quite close to the informality on paper. We have shown this in
formalisations for the CR-property in the lambda-calculus (following
the proof Barendregt's book and I think this is the one you follow, just
with de Bruijn indices), for SN in the simply-typed lambda-calculus
(following Girard's Proofs and Types Book), various proofs from
SOS and a complete formalisation of a chapter by Crary on logical
relations. I do not foresee any problems to reuse the nominal package
for your formalisation. What you gain is that your proofs look more
like what one would write down on paper. If we can be of any assistance,
please let us know.
Florian Kammueller writes:
> 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
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and