On Isomorphisms of Intersection Types (2009)
Mariangiola Dezani-ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Abstract. The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of...
Normalisation is Insensible to λ-term Identity or Difference (2008)
This paper analyses the computational behaviour of λterm applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation...
A Behavioural Model for Klop’s Calculus (2006)
Mariangiola Dezani-ciancaglini, Makoto Tatsuta
Replace this file withprentcsmacro.sty for your meeting, or withentcsmacro.sty for your meeting. Both can be
Strong normalization proof with CPS-translation for second order classical natural deduction (2003)
Nakazawa, Koji, Tatsuta, Makoto
This paper points out an error of Parigot’s proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation,...