Programming with proofs: A second order type theory

This publication has 6 references indexed in Scilit:

• Constructive Mathematics and Computer Programming
  Published by Elsevier ,2014
• The system F of variable types, fifteen years later
  Theoretical Computer Science, 1986
• Constructions: A higher order proof system for mechanizing mathematics
  Published by Springer Nature ,1985
• The categorical abstract machine
  Published by Springer Nature ,1985
• 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
• An Abstract Notion of Realizability for Which Intuitionistic Predicate Calculus is Complete
  Published by Elsevier ,1970