Categorical Logic and Type Theory, Volume 141Gulf Professional Publishing, 10 mei 2001 - 778 pagina's This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists. |
Inhoudsopgave
Prospectus | 1 |
Introduction to fibred category theory | 19 |
Simple type theory | 119 |
Equational Logic | 169 |
First order predicate logic | 219 |
Higher order predicate logic | 311 |
The effective topos | 373 |
Internal category theory | 407 |
Polymorphic type theory | 441 |
Advanced fibred category theory | 509 |
First order dependent type theory | 581 |
Higher order dependent type theory | 645 |
References | 717 |
| 735 | |
| 743 | |
Overige edities - Alles bekijken
Veelvoorkomende woorden en zinsdelen
adjunction algebra Assume base category Beck-Chevalley Beck-Chevalley condition C₁ Cartesian closed Cartesian morphism Cartesian products change-of-base codomain fibration commuting comonad comprehension category Consider construction coproducts correspondence define Definition dependent type theory described diagram effective topos Eq-fibration equaliser equality equations equivalence example Exercise exponents Fam(C family fibration fibred categories fibred functor finite limits Frobenius full and faithful function symbols indexed category internal category isomorphism kinds left adjoint Lemma mono natural numbers natural transformation obtained pair polymorphic type theory predicate logic preorder preserves products and coproducts projection Proof Prop Proposition pullback quantification quotient types relation result right adjoint Sets Show signature simple fibration simple type theory split fibration strong structure Sub(B subobject fibration subset types terminal object Theorem topos total category type context UFam(PER UFam(w-Sets unique variables vertical w-Sets yields
Populaire passages
Pagina 719 - A. Carboni, S. Lack, and RFC Walters. Introduction to extensive and distributive categories.
Pagina 719 - JRB Cockett and D. Spencer. Strong categorical datatypes I. In RAG Seely, editor, Category Theory 1991, number 13 in CMS Conference Proceedings, pages 141-169, 1992.
Pagina 725 - In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of Electronic Notes in Theoretical Computer Science, Tulane University, New Orleans, Louisiana, Mar.
Pagina 719 - About charity. Technical Report 92/480/18, Dep. Comp. Sci., Univ. Calgary, 1992. [5] JRB Cockett and D. Spencer. Strong categorical datatypes I. In RAG Seely, editor, Category Theory 1991, volume 13 of CMS Conference Proceedings, pages 141-169.
Verwijzingen naar dit boek
Logics for Coalgebras and Applications to Computer Science Alexander Kurz Gedeeltelijke weergave - 2001 |