Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
A constructive semantic approach to cut elimination in type theories with axioms
Year:2008
Research Areas
  • Programming language
Information
Abstract
We give a fully constructive semantic proof of cut elimination for intuitionistic type theory with axioms. The problem here, as with the original Takeuti conjecture, is that the impredicativity of the formal system involved makes it impossible to define a semantics along conventional lines, in the absence, a priori, of cut, or to prove completeness by induction on subformula structure. In addition, unlike semantic proofs by Tait, Takahashi, and Andrews of variants of the Takeuti conjecture, our arguments are constructive. Our techniques offer also an easier approach than Girard’s strong normalization techniques to the problem of extending the cut-elimination result in the presence of axioms. We need only to relativize the Heyting algebras involved in a straightforward way.
International
Si
Congress
22nd International Workshop, CSL 2008.
960
Place
Reviewers
No
ISBN/ISSN
978-3-540-87530-7
10.1007/978-3-540-87531-4
Start Date
16/09/2008
End Date
19/09/2008
From page
169
To page
183
22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings.
Participants
  • Autor: Olivier Hermant (Université Paris VII - Denis Diderot, Francia)
  • Autor: James Lipton . (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2019 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)