[isabelle] Sigma-calculus in Isabelle/HOL

Hi Florian,

Are you aware of all the recent developments in the nominal 
datatype package? 

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.

Best wishes,

Florian Kammueller writes:
 > 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

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