Skip to main content
SpringerLink
Log in

On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem

  • Conference paper
  • First Online:
Book cover Types for Proofs and Programs (TYPES 2000)

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

Included in the following conference series:

Abstract

In this paper we relate the lax modality Ο to Intuitionistic Propositional Logic (IPL) and give a complete characterisation of inhabitation in Computational Type Theory (CTT) as a logic of constraint contexts. This solves a problem open since the 1940’s, when Curry was the first to suggest a formal syntactic interpretation of Ο in terms of contexts.

This work is supported by EPSRC grants GR/L86180 and GR/M99637, by the EU Types Working Group IST-EU-29001 and by the British Council.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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.

References

  1. P. Aczel. The Russell-Prawitz modality. Mathematical Structures in Computer Science, 11(4), 2001. Special issue: Modalities in Type Theory (Proceedings of the 1999 Workshop on Intuitionistic Modal Logic and Applications, Trento, Italy).

    Google Scholar 

  2. N. Benton and V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2), March 1998.

    Google Scholar 

  3. P. N. Benton. A unified approach to strictness analysis and optimising transformations. Technical Report 388, University of Cambridge Computer Laboratory, February 1996.

    Google Scholar 

  4. H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.

    Article  MATH  MathSciNet  Google Scholar 

  5. H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.

    Google Scholar 

  6. R. Davies and F. Pfenning. A modal analysis of staged computation. In Jr. Guy Steele, editor, Proc. 23rd POPL. ACM Press, January 1996.

    Google Scholar 

  7. J. Despeyroux and P. Leleu. Recursion over objects of functional type. Mathematical Structures in Computer Science, 2001.

    Google Scholar 

  8. J. Despeyroux, F. Pfenning, and C. Schürmann. Primitive recursion for higherorder abstract syntax. In Typed Lambda Calculi and Applications, pages 147–163. Springer, 1997. LNCS 1210.

    Google Scholar 

  9. M. Fairtlough and M. Mendler. Propositional Lax Logic. Information and Computation, 137(1):1–33, August 1997.

    Article  MATH  MathSciNet  Google Scholar 

  10. M.V.H. Fairtlough and M. Walton. Quantified Lax Logic. Technical Report CS-97-11, Department of Computer Science, The University of Sheffield, July 1997.

    Google Scholar 

  11. R. I. Goldblatt. Grothendieck topology as geometric modality. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 27:495–529, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  12. J. Hatcli. and O. Danvy. A computational formalisation for partial evaluation. Math. Struct. in Comp. Science, 7:507–541, 1997.

    Article  Google Scholar 

  13. B. P. Hilken. Duality for intuitionistic modal algebras. UMCS-96-12-2, Manchester University, Department of Computer Science, 1996. To appear in Journal of Pure and Applied Algebra.

    Google Scholar 

  14. P. T. Johnstone. Stone Spaces. Cambridge University Press, 1982.

    Google Scholar 

  15. D. S. Macnab. Modal operators on Heyting algebras. Algebra Universalis, 12:5–29, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  16. M. Mendler. Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification. In G. Jones and M. Sheeran, editors, Workshop on Designing Correct Circuits. Springer, 1991.

    Google Scholar 

  17. M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Department of Computer Science, University of Edinburgh, ECS-LFCS-93-255, March 1993.

    Google Scholar 

  18. E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  19. D. A. Turner. Elementary strong functional programming. In P. H. Hartel and M. J. Plasmeijer, editors, Functional Programming Languages in Education FPLE’95, pages 1–13. Springer, 1995. LNCS 1022.

    Google Scholar 

  20. P. Wadler. Comprehending monads. In Conference on Lisp and Functional Programming. ACM Press, June 1990.

    Google Scholar 

  21. P. Wadler. Monads for functional programming. In Lecture Notes for the Marktoberdorf Summer School on Program Design Calculi. Springer Verlag, August 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Sheffield University, 211 Portobello Street, S1 4DP, Sheffield, UK

    Matt Fairtlough & Michael Mendler

Authors
  1. Matt Fairtlough
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK

    Paul Callaghan , Zhaohui Luo , James McKinna  & Robert Pollack , ,  & 

  2. Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, EH9 3JZ, Edinburgh, Scotland, UK

    Robert Pollack

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fairtlough, M., Mendler, M. (2002). On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds) Types for Proofs and Programs. TYPES 2000. Lecture Notes in Computer Science, vol 2277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45842-5_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-45842-5_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43287-6

  • Online ISBN: 978-3-540-45842-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation