Email Gateway (Aug 18 2022 at 10:05): Email Gateway (Aug 18 2022 at 10:05):From: Christian Urban <urbanc@in.tum.de>
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,
Christian
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
Last updated: May 03 2024 at 04:19 UTC