Pure type systems with explicit substitutions

We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivale...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Fridlender, Daniel, Pagano, Miguel
Formato: article
Lenguaje:Inglés
Publicado: 2022
Materias:
Predicative PTS
Normalisation by evaluation
Conversion
Acceso en línea:http://hdl.handle.net/11086/27605
https://doi.org/10.1017/S0956796815000210
https://doi.org/10.1017/S0956796815000210
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba

Ejemplares similares

Ejemplares similares