In this thesis is shown a proof of canonical normal form theorem for the type theory of regular categories. The theorem states that any closed typed term, whose derivation has no open assumption, can be reduced by a sequence of reductions into an equivalent one in canonical form and that the proof of any provable judgement can be transformed into an equivalent one in introductory form.
In this thesis is shown a proof of canonical normal form theorem for the type theory of regular categories. The theorem states that any closed typed term, whose derivation has no open assumption, can be reduced by a sequence of reductions into an equivalent one in canonical form and that the proof of any provable judgement can be transformed into an equivalent one in introductory form.
A canonical normal form theorem for the type theory of regular categories
BORSETTO, RICCARDO
2022/2023
Abstract
In this thesis is shown a proof of canonical normal form theorem for the type theory of regular categories. The theorem states that any closed typed term, whose derivation has no open assumption, can be reduced by a sequence of reductions into an equivalent one in canonical form and that the proof of any provable judgement can be transformed into an equivalent one in introductory form.File  Dimensione  Formato  

Borsetto_Riccardo.pdf
accesso aperto
Dimensione
544.04 kB
Formato
Adobe PDF

544.04 kB  Adobe PDF  Visualizza/Apri 
The text of this website © Università degli studi di Padova. Full Text are published under a nonexclusive license. Metadata are under a CC0 License
https://hdl.handle.net/20.500.12608/46210