Hostname: page-component-745bb68f8f-f46jp Total loading time: 0 Render date: 2025-01-12T11:01:38.730Z Has data issue: false hasContentIssue false
  • English
  • Français

On cubism

Part of: JFP Research Articles

Published online by Cambridge University Press:  07 November 2008

Bart Jacobs
Bart Jacobs
Affiliation:
CWI,Kruislaan 413, 1098 SJ Amsterdam, The Netherlands.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

A number of difficulties in the formalism of Pure Type Systems (PTS) is discussed and an alternative classification system for typed calculi is proposed. In the new approach the main novelty is that one first explicitly specifies the dependencies that may occur. This is especially useful to describe constants, but it also facilitates the description of other type theoretic features like dependent sums.

Type
Articles
Information
Journal of Functional Programming , Volume 6 , Issue 3 , May 1996 , pp. 379 - 392
Copyright
Copyright © Cambridge University Press 1996

References

Barendregt, H. P. (1992) Lambda calculi with types. In: Abramski, S., Gabbai, Dov M. and Maibaum, T. S. E. (eds.), Handbook of Logic in Computer Science, Vol. 2, Oxford University Press, pp. 117–309.Google Scholar
Church, A. (1940) A formulation of the simple theory of types. J. Symbol. Log. 5: 56–68.CrossRefGoogle Scholar
Coquand, Th. and Huet, G. (1988) The Calculus of Constructions. Inform. & Comp., 76(2/3): 95–120.CrossRefGoogle Scholar
Geuvers, J. H. (1993) Logics and Type Systems. PhD Thesis, University of Nijmegen.Google Scholar
Jacobs, B. (1991) Categorical Type Theory. PhD Thesis, University of Nijmegen.Google Scholar
Jacobs, B. and Melham, T. (1993) Translating dependent type theory into higher order logic. In Bezem, M. and Groote, J.F. (eds.), Typed Lambda Calculi and Applications. Springer LNCS 664 pp. 209–229.CrossRefGoogle Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory. Bibliopolis, Naples.Google Scholar
Moggi, E. (1991) A category-theoretic account of program modules. Math. Struct. in Comp. Sci., 1(1): 103–139.CrossRefGoogle Scholar
Pavlović, D. (1990) Predicates and Fibrations. PhD Thesis, University of Utrecht.Google Scholar
Pavlović, D. (1991) Constructions and predicates. In Pitt, D.H. et al. (eds.), Category and Computer Science: Springer LNCS 530, pp. 173–196.CrossRefGoogle Scholar
Phoa, W. (1992) An introduction to fibrations, topos theory, the effective topos and modest sets. Techn. Rep. LFCS–92–208, Edinburgh University.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.