Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions

We will present a Logic of Computable Functions based on the idea of Synthetic Domain Theory such that all functions are automatically continuous. Its implementation in the Lego proof-checker

• Type: Conference
• Year: 1996
• Where: TPHOL
• Authors: Bernhard Reus
• Keywords: Automated Reasoning, Machine Checked Proofs, Powerful Type Theory, Synthetic Domain Theory, TPHOL 1996