Sciweavers

13

TPHOL
1996
IEEE

76views Automated Reasoning» more TPHOL 1996»

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

13 years 9 months ago

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

Download www.cogs.susx.ac.uk

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 pr...

Bernhard Reus

claim paper

Read More »

17

TPHOL
1996
IEEE

88views Automated Reasoning» more TPHOL 1996»

Importing Mathematics from HOL into Nuprl

13 years 9 months ago

Importing Mathematics from HOL into Nuprl

Download www.nuprl.org

Nuprl and HOL are both tactic-based interactive theorem provers for higher-order logic, and both have been used in many substantial applications over the last decade. However, the ...

Douglas J. Howe

claim paper

Read More »

17

TPHOL
1996
IEEE

114views Automated Reasoning» more TPHOL 1996»

Five Axioms of Alpha-Conversion

13 years 9 months ago

Five Axioms of Alpha-Conversion

Download www.cs.haverford.edu

Andrew D. Gordon, Thomas F. Melham

claim paper

Read More »