Pure type systems with explicit substitutions

Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.

Bibliographic Details
Main Authors: Fridlender, Daniel, Pagano, Miguel
Format: publishedVersion
Language:eng
Published: 2022
Subjects:
Online Access:http://hdl.handle.net/11086/27605
https://doi.org/10.1017/S0956796815000210
_version_ 1801214700696895488
author Fridlender, Daniel
Pagano, Miguel
author_facet Fridlender, Daniel
Pagano, Miguel
author_sort Fridlender, Daniel
collection Repositorio Digital Universitario
description Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
format publishedVersion
id rdu-unc.27605
institution Universidad Nacional de Cordoba
language eng
publishDate 2022
record_format dspace
spelling rdu-unc.276052022-10-13T11:08:42Z Pure type systems with explicit substitutions Fridlender, Daniel Pagano, Miguel Predicative PTS Normalisation by evaluation Conversion publishedVersion Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. 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 η. http://journals.cambridge.org/article_S0956796815000210 publishedVersion Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Ciencias de la Computación 2022-07-27T20:50:13Z 2015 article http://hdl.handle.net/11086/27605 https://doi.org/10.1017/S0956796815000210 https://doi.org/10.1017/S0956796815000210 eng Attribution-NonCommercial-NoDerivatives 4.0 International restrictedAccess http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso; Electrónico y/o Digital ISSN: 1469-7653
spellingShingle Predicative PTS
Normalisation by evaluation
Conversion
Fridlender, Daniel
Pagano, Miguel
Pure type systems with explicit substitutions
title 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_short Pure type systems with explicit substitutions
title_sort pure type systems with explicit substitutions
topic Predicative PTS
Normalisation by evaluation
Conversion
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