Typechecking dependent types and subtypes

This publication has 8 references indexed in Scilit:

• A theory of type polymorphism in programming
  Published by Elsevier ,2003
• Abstract types have existential types
  Published by Association for Computing Machinery (ACM) ,1985
• Three approaches to type structure
  Published by Springer Nature ,1985
• Constructions: A higher order proof system for mechanizing mathematics
  Published by Springer Nature ,1985
• A kernel language for abstract data types and modules
  Published by Springer Nature ,1984
• An efficient interpreter for the lambda-calculus
  Journal of Computer and System Sciences, 1981
• An Intuitionistic Theory of Types: Predicative Part
  Published by Elsevier ,1975
• Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types
  Published by Elsevier ,1971