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

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