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 › peer review

53 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

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Accesso al documento

OA Link

Fingerprint Entra nei temi di ricerca di 'Wellfounded Trees and Dependent Polynomial Functors'. Insieme formano una fingerprint unica.

Cita questo

@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 -