dc.contributor.author | Fridlender, Daniel | |
dc.contributor.author | Pagano, Miguel | |
dc.date.accessioned | 2022-07-27T20:50:13Z | |
dc.date.issued | 2015 | |
dc.identifier.uri | http://hdl.handle.net/11086/27605 | |
dc.description.abstract | 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 η. | en |
dc.description.uri | http://journals.cambridge.org/article_S0956796815000210 | |
dc.format.medium | Impreso; Electrónico y/o Digital | |
dc.language.iso | eng | es |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 International | * |
dc.rights | restrictedAccess | |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.source | ISSN: 1469-7653 | |
dc.subject | Predicative PTS | en |
dc.subject | Normalisation by evaluation | en |
dc.subject | Conversion | en |
dc.title | Pure type systems with explicit substitutions | en |
dc.type | article | es |
dc.description.version | publishedVersion | es |
dc.description.fil | Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. | es |
dc.description.fil | Fil: Pagano, Miguel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. | es |
dc.journal.city | Cambridge | es |
dc.journal.country | Reino Unido | es |
dc.journal.editorial | Cambridge University Press | es |
dc.journal.pagination | 1-30 | es |
dc.journal.referato | Con referato | |
dc.journal.title | Journal of Functional Programming | es |
dc.journal.volume | 25 | es |
dc.description.field | Ciencias de la Computación | |
dc.identifier.url | https://doi.org/10.1017/S0956796815000210 | |
dc.identifier.doi | https://doi.org/10.1017/S0956796815000210 | |