Wellfounded Trees and Dependent Polynomial Functors

Nicola Gambino; Nicola Gambino; Martin Hyland

Wellfounded Trees and Dependent Polynomial Functors

Nicola Gambino, Nicola Gambino, Martin Hyland

Matematica e Informatica

Risultato della ricerca: Other

52 Citazioni (Scopus)

Abstract

We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.

Lingua originale	English
Numero di pagine	15
Stato di pubblicazione	Published - 2004

Fingerprint

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Cita questo

Gambino, N., Gambino, N., & Hyland, M. (2004). Wellfounded Trees and Dependent Polynomial Functors.

@conference{2334b74029b34093ba86546194744a2b,

title = "Wellfounded Trees and Dependent Polynomial Functors",

abstract = "We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.",

keywords = "Wellfounded trees, categorical logic, locally cartesian closed categories, Wellfounded trees, categorical logic, locally cartesian closed categories",

author = "Nicola Gambino and Nicola Gambino and Martin Hyland",

year = "2004",

language = "English",

}

TY - CONF

T1 - Wellfounded Trees and Dependent Polynomial Functors

AU - Gambino, Nicola

AU - Hyland, Martin

PY - 2004

Y1 - 2004

N2 - We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.

AB - We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.

KW - Wellfounded trees

KW - categorical logic

KW - locally cartesian closed categories

KW - Wellfounded trees

KW - categorical logic

KW - locally cartesian closed categories

UR - http://hdl.handle.net/10447/40056

M3 - Other

ER -

Accesso al documento

OA Link