Pure type systems with explicit substitutions
Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
| Main Authors: | , |
|---|---|
| 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 |