Lambda Definability with Sums via Grothendieck Logical Relations | SpringerLink
Skip to main content
Springer Nature Link
Log in

Lambda Definability with Sums via Grothendieck Logical Relations

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1581))

Included in the following conference series:

  • 634 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Alimohamed. A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science, 146:5–23, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. D. Dougherty and R. Subrahmanyam. Equality between functionals in the presence of coproducts. Submitted to Information and Computation. An earlier version appeared in Proceedings of 10th LICS, pages 282–291, 1995.

    Google Scholar 

  3. N. Ghani. βη-equality for coproducts. In Typed Lambda Calculi and Applications, Proceedings of TLCA’ 95, pages 171–185. Springer LNCS 902, 1995.

    Chapter  Google Scholar 

  4. A. Jung and J. Tiuryn. A new characterisation of lambda definability. In Typed Lambda Calculi and Applications, Proceedings of TLCA’ 93, pages 230–244. Springer LNCS 664, 1993.

    Chapter  Google Scholar 

  5. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

    Google Scholar 

  6. S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

    Google Scholar 

  7. J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume II, pages 365–458. Elsevier Science Publishers, 1990.

    Google Scholar 

  8. P.W. O’Hearn and J.G. Riecke. Kripke logical relations and PCF. Information and Computation, 120:107–116, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  9. E. Palmgren. Constructive sheaf semantics. Mathematical Logic Quarterly, 43:321–325, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  10. G.D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980.

    Google Scholar 

  11. J.G. Riecke and A.B. Sandholm. A relational account of call-by-value sequentiality. In Proceedings of 12th Annual Symposium on Logic in Computer Science, pages 258–267, 1997.

    Google Scholar 

  12. G. Wraith. Artin glueing. Journal of Pure and Applied Algebra, 4:345–348, 1974.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. COGS, University of Sussex, Brighton, UK

    Marcelo Fiore

  2. LFCS, Division of Informatics, University of Edinburgh, Edinburgh, UK

    Alex Simpson

Authors
  1. Marcelo Fiore
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alex Simpson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS - UPR9016, Institut de Mathématiques de Luminy, 163 Avenue de Luminy, case 907, F-13288, Marseille cedex 9, France

    Jean-Yves Girard

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fiore, M., Simpson, A. (1999). Lambda Definability with Sums via Grothendieck Logical Relations. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-48959-2_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65763-7

  • Online ISBN: 978-3-540-48959-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation