Lambda Definability with Sums via Grothendieck Logical Relations

Marcelo P. Fiore, Alex Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary.
Original languageEnglish
Title of host publicationProceedings of the 4th International Conference on Typed Lambda Calculi and Applications
Place of PublicationLondon, UK, UK
PublisherSpringer-Verlag GmbH
Pages147-161
Number of pages15
DOIs
Publication statusPublished - 1999

Publication series

NameTLCA '99
PublisherSpringer-Verlag

Fingerprint

Dive into the research topics of 'Lambda Definability with Sums via Grothendieck Logical Relations'. Together they form a unique fingerprint.

Cite this