Publikationsansicht

Modelling General Recursion in Type Theory (2002)

Abstract

Constructive type theory is an expressive programming language where both algorithms and proofs can be represented. However, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination.

Details der Publikation

Download	http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.6947
Quelle	http://www.math.chalmers.se/~bove/Papers/general_presentation.ps.gz
Mitarbeiter	CiteSeerX
Archiv	CiteSeerX - Scientific Literature Digital Library and Search Engine (United States)
Typ	text
Sprache	Englisch
Verknüpfungen	10.1.1.6.4575, 10.1.1.36.7155, 10.1.1.42.8429, 10.1.1.32.1831, 10.1.1.38.4421, 10.1.1.32.6626, 10.1.1.93.5387, 10.1.1.6.6779, 10.1.1.63.4242, 10.1.1.8.6461, 10.1.1.6.2892, 10.1.1.62.1751, 10.1.1.111.8864, 10.1.1.62.6743, 10.1.1.113.2661, 10.1.1.124.5818, 10.1.1.102.2326, 10.1.1.66.561, 10.1.1.77.1017, 10.1.1.81.7534, 10.1.1.92.685, 10.1.1.117.2495, 10.1.1.118.6224, 10.1.1.119.6810, 10.1.1.121.4698, 10.1.1.130.1775, 10.1.1.15.6924, 10.1.1.7.3465, 10.1.1.5.4512, 10.1.1.139.8925