Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft
- 1 January 1989
- book chapter
- Published by Springer Nature
- p. 241-256
- https://doi.org/10.1007/3-540-50940-2_39
Abstract
No abstract availableKeywords
This publication has 17 references indexed in Scilit:
- Characterization of typings in polymorphic type disciplinePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A categorical semantics of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The essence of MLPublished by Association for Computing Machinery (ACM) ,1988
- Using dependent types to express modular structurePublished by Association for Computing Machinery (ACM) ,1986
- Abstract types have existential typesPublished by Association for Computing Machinery (ACM) ,1985
- Constructions: A higher order proof system for mechanizing mathematicsPublished by Springer Nature ,1985
- Type inference and type containmentPublished by Springer Nature ,1984
- Executable specification of static semanticsPublished by Springer Nature ,1984
- Principal type-schemes for functional programsPublished by Association for Computing Machinery (ACM) ,1982
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940