Lambda Definability with Sums via Grothendieck Logical Relations

Marcelo P. Fiore, Alex Simpson

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


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
Number of pages15
Publication statusPublished - 1999

Publication series

NameTLCA '99


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

Cite this