Pure type systems with de Bruijn indices

Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been in...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Kamareddine, F., Ríos, A.
Formato:	JOUR
Materias:	Computer programming languages Computer science Formal logic Mathematical techniques Theorem proving Automath systems Dependent theory Edinburgh logical frameworks Polymorphic theory Pure type systems System theory
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_00104620_v45_n2_p187_Kamareddine
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_00104620_v45_n2_p187_Kamareddine
record_format	dspace
spelling	todo:paper_00104620_v45_n2_p187_Kamareddine2023-10-03T14:09:04Z Pure type systems with de Bruijn indices Kamareddine, F. Ríos, A. Computer programming languages Computer science Formal logic Mathematical techniques Theorem proving Automath systems Dependent theory Edinburgh logical frameworks Polymorphic theory Pure type systems System theory Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been introduced independently by Terlouw and Berardi in order to provide a unified formalism in which many type systems can be represented. In particular, PTSs allow the representation of the simple theory of types, the polymophic theory of types, the dependent theory of types and various other well-known type systems such as the Edinburgh Logical Frameworks and the Automath system. PTSs are usually presented using variable names. In this article, we present a formulation of PTSs with de Bruijn indices. De Bruijn indices avoid the problems caused by variable names during the implementation of type systems. We show that PTSs with variable names and PTSs with de Bruijn indices are isomorphic. This isomorphism enables us to answer questions about PTSs with de Bruijn indices including confluence, termination (strong normalization) and safety (subject reduction). JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00104620_v45_n2_p187_Kamareddine
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Computer programming languages Computer science Formal logic Mathematical techniques Theorem proving Automath systems Dependent theory Edinburgh logical frameworks Polymorphic theory Pure type systems System theory
spellingShingle	Computer programming languages Computer science Formal logic Mathematical techniques Theorem proving Automath systems Dependent theory Edinburgh logical frameworks Polymorphic theory Pure type systems System theory Kamareddine, F. Ríos, A. Pure type systems with de Bruijn indices
topic_facet	Computer programming languages Computer science Formal logic Mathematical techniques Theorem proving Automath systems Dependent theory Edinburgh logical frameworks Polymorphic theory Pure type systems System theory
description	Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been introduced independently by Terlouw and Berardi in order to provide a unified formalism in which many type systems can be represented. In particular, PTSs allow the representation of the simple theory of types, the polymophic theory of types, the dependent theory of types and various other well-known type systems such as the Edinburgh Logical Frameworks and the Automath system. PTSs are usually presented using variable names. In this article, we present a formulation of PTSs with de Bruijn indices. De Bruijn indices avoid the problems caused by variable names during the implementation of type systems. We show that PTSs with variable names and PTSs with de Bruijn indices are isomorphic. This isomorphism enables us to answer questions about PTSs with de Bruijn indices including confluence, termination (strong normalization) and safety (subject reduction).
format	JOUR
author	Kamareddine, F. Ríos, A.
author_facet	Kamareddine, F. Ríos, A.
author_sort	Kamareddine, F.
title	Pure type systems with de Bruijn indices
title_short	Pure type systems with de Bruijn indices
title_full	Pure type systems with de Bruijn indices
title_fullStr	Pure type systems with de Bruijn indices
title_full_unstemmed	Pure type systems with de Bruijn indices
title_sort	pure type systems with de bruijn indices
url	http://hdl.handle.net/20.500.12110/paper_00104620_v45_n2_p187_Kamareddine
work_keys_str_mv	AT kamareddinef puretypesystemswithdebruijnindices AT riosa puretypesystemswithdebruijnindices
_version_	1807321718679666688

Pure type systems with de Bruijn indices

Ejemplares similares