The weak normalization of the simply typed λse-calculus

Mostrar todas las versiones(2)

In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomo...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Arbiser, A., Kamareddine, F., Rios, A.
Formato:	JOUR
Materias:	Explicit substitution Lambda calculus Normalization Simple typing
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_13670751_v15_n2_p121_Arbiser
record_format	dspace
spelling	todo:paper_13670751_v15_n2_p121_Arbiser2023-10-03T16:11:23Z The weak normalization of the simply typed λse-calculus Arbiser, A. Kamareddine, F. Rios, A. Explicit substitution Lambda calculus Normalization Simple typing In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomorphic to λse→. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the λσ-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus λω′e which works like λse but which is closer to λσ than λωe. For both λωe and λω′e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all λσ open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Explicit substitution Lambda calculus Normalization Simple typing
spellingShingle	Explicit substitution Lambda calculus Normalization Simple typing Arbiser, A. Kamareddine, F. Rios, A. The weak normalization of the simply typed λse-calculus
topic_facet	Explicit substitution Lambda calculus Normalization Simple typing
description	In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomorphic to λse→. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the λσ-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus λω′e which works like λse but which is closer to λσ than λωe. For both λωe and λω′e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all λσ open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved.
format	JOUR
author	Arbiser, A. Kamareddine, F. Rios, A.
author_facet	Arbiser, A. Kamareddine, F. Rios, A.
author_sort	Arbiser, A.
title	The weak normalization of the simply typed λse-calculus
title_short	The weak normalization of the simply typed λse-calculus
title_full	The weak normalization of the simply typed λse-calculus
title_fullStr	The weak normalization of the simply typed λse-calculus
title_full_unstemmed	The weak normalization of the simply typed λse-calculus
title_sort	weak normalization of the simply typed λse-calculus
url	http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser
work_keys_str_mv	AT arbisera theweaknormalizationofthesimplytypedlsecalculus AT kamareddinef theweaknormalizationofthesimplytypedlsecalculus AT riosa theweaknormalizationofthesimplytypedlsecalculus AT arbisera weaknormalizationofthesimplytypedlsecalculus AT kamareddinef weaknormalizationofthesimplytypedlsecalculus AT riosa weaknormalizationofthesimplytypedlsecalculus
_version_	1807323663900344320

The weak normalization of the simply typed λse-calculus

Ejemplares similares