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

13 years 8 months ago

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 proof-checker

Bernhard Reus

Real-time Traffic

Automated Reasoning | Machine Checked Proofs | Powerful Type Theory | Synthetic Domain Theory | TPHOL 1996 |

claim paper

» The Fixed Point Property in Synthetic Domain Theory

» Computing with functionals computability theory or computer science

» Towards Computability of Higher Type Continuous Data

» Embedding a logical theory of constructions in Agda

» HOLCF Higher Order Logic of Computable Functions

» Type Theory and Functional Programming

» Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory

» A type theory for probability density functions

Post Info
More Details (n/a)

Added	07 Aug 2010
Updated	07 Aug 2010
Type	Conference
Year	1996
Where	TPHOL
Authors	Bernhard Reus

Comments (0)

Sciweavers

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

Automated Reasoning | Machine Checked Proofs | Powerful Type Theory | Synthetic Domain Theory | TPHOL 1996 |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers