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

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
id I10-R141-11086-27605
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Predicative PTS
Normalisation by evaluation
Conversion
spellingShingle Predicative PTS
Normalisation by evaluation
Conversion
Fridlender, Daniel
Pagano, Miguel
Pure type systems with explicit substitutions
topic_facet Predicative PTS
Normalisation by evaluation
Conversion
description 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 equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.
format article
author Fridlender, Daniel
Pagano, Miguel
author_facet Fridlender, Daniel
Pagano, Miguel
author_sort Fridlender, Daniel
title Pure type systems with explicit substitutions
title_short Pure type systems with explicit substitutions
title_full Pure type systems with explicit substitutions
title_fullStr Pure type systems with explicit substitutions
title_full_unstemmed Pure type systems with explicit substitutions
title_sort pure type systems with explicit substitutions
publishDate 2022
url http://hdl.handle.net/11086/27605
https://doi.org/10.1017/S0956796815000210
https://doi.org/10.1017/S0956796815000210
work_keys_str_mv AT fridlenderdaniel puretypesystemswithexplicitsubstitutions
AT paganomiguel puretypesystemswithexplicitsubstitutions
bdutipo_str Repositorios
_version_ 1764820391427047425

Ejemplares similares