Peter Hancock  @ NUS Home/Search
Context Related
| lfcs.inf.ed.ac.uk/...LFCS00421.ps.gz Cached: PS.gz PS PDF Image Update Help From: lfcs.inf.ed.ac.uk/reports...index (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: The work reported in this thesis arises from the old idea, going back to the origins of constructive logic, that a proof is fundamentally a kind of program. (Update)
Cited by: More
Pierre Hyvernat - Interactive Programs In (Correct)
Active bibliography (related documents): More All
19.4: Ordinals and Interactive Programs - Hancock (2000) (Correct)
4.0: The AMEN architecture. - Peter Hancock Abandoned (Correct)
0.7: Induction-Recursion and Initial Algebras - Dybjer, Setzer (2000) (Correct)
Similar documents based on text: More All
0.1: Interactive Programs in Dependent Type Theory - Hancock, Setzer, Clerk (2000) (Correct)
0.1: On Bounded Set Theory - Sazonov (1997) (Correct)
0.1: Spikes, Synchrony, Sequences and - David Sterratt Doctor (Correct)
BibTeX entry: (Update)
Peter Hancock. Ordinals and Interactive Programs. PhD dissertation, University of Edinburgh, 2000. http://citeseer.comp.nus.edu.sg/669645.html More
@misc{ hancock00ordinals,
author = "P. Hancock",
title = "Ordinals and Interactive Programs",
text = "Peter Hancock. Ordinals and Interactive Programs. PhD dissertation, University
of Edinburgh, 2000.",
year = "2000",
url = "citeseer.comp.nus.edu.sg/669645.html" }
Citations (may not include all citations):1933 Communication and Concurrency (context) - Milner - 1989
809 A theory of type polymorphism in programming (context) - Milner - 1978
652 A Discipline of Programming (context) - Dijkstra - 1976
502 Concurrency and automata on infinite sequences (context) - Park - 1981
434 A framework for defining logics - Harper, Honsell et al. - 1987
369 Information and Computation (context) - Moggi, computation - 1991
293 The essence of functional programming - Wadler - 1992
194 The Formal Semantics of Programming Languages (context) - Winskel - 1993
185 The Calculi of Lambda Conversion (context) - Church - 1941
124 Monads for functional programming - Wadler - 1995
124 Monads for functional programming - Wadler - 1994
104 Algebra of Programming (context) - Bird, de Moor - 1997
97 An introduction to inductive definitions (context) - Aczel - 1977
96 An algorithm for testing conversion in type theory (context) - Coquand - 1991
91 Refinement Calculus: a systematic introduction (context) - Back, von Wright - 1998
91 Program development by stepwise refinement (context) - Wirth - 1971
90 Type systems - Cardelli - 1997
78 Texts and Monographs in Computer Science (context) - Dijkstra, Scholten et al. - 1989
67 Recursive Programming Techniques (context) - Burge - 1975
65 Sheaves in Geometry and Logic: A First Introduction to Topos.. (context) - Lane, Moerdijk - 1992
62 How to declare an imperative - Wadler - 1995
56 The formulas-as-types notion of construction (context) - Howard - 1980
46 Proof Theory and Logical Complexity (context) - Girard - 1987
45 Cambridge University Press (context) - Huet, Plotkin et al. - 1993
45 Cambridge University Press (context) - Huet, Plotkin et al. - 1991
38 Constructive mathematics and computer programming (context) - Martin-Lof - 1979
38 Semantics of interaction - Abramsky - 1997
28 Intuitionistic Type Theory (context) - Martin-Lof - 1984
26 volume 43 of Cambridge Tracts in Theoretical Computer Scienc.. (context) - Troelstra, Schwichtenburg et al. - 1996
26 Springer-Verlag (context) - Conway, Guy et al. - 1996
26 Elements of Intuitionism (context) - Dummett - 1977
26 volume 43 of Cambridge Tracts in Theoretical Computer Scienc.. (context) - Troelstra, Schwichtenberg et al. - 1996
25 A general formulation of simultaneous inductive-recursive de.. - Dybjer - 1997
22 On universes in type theory (context) - Palmgren - 1998
21 An algebraic construction of predicate transformers - Gardiner, Martin et al. - 1994
21 Programming in MartinL of's Type Theory (context) - Nordstrom, Smith - 1990
19 Iterated inductive fixed-point theories: Application to hanc.. (context) - Feferman - 1982
19 Computation and Reasoning (context) - Luo - 1994
19 recursion and course-of-values (context) - Uustalu, Vene et al. - 1999
19 Iterated inductive fixed-point theories: Application to Hanc.. (context) - Feferman - 1982
16 Zur deutung der intuitionistischen logik (context) - Kolmogorov - 1932
15 Zur konstruktion von ordnungszahlen (context) - Neumer - 1954
15 Zur konstruktion von ordnungszahlen (context) - Neumer - 1954
15 Zur konstruktion von ordnungszahlen (context) - Neumer - 1953
15 Syntax and Semantics of Dependent Types - Hofmann - 1997
15 Zur konstruktion von ordnungszahlen (context) - Neumer - 1956
15 Zur konstruktion von ordnungszahlen (context) - Neumer - 1954
14 Conceptual Mathematics: A First Introduction to Categories (context) - Lawvere, Schanuel - 1997
13 Generalised Algebraic Theories and Contextual Categories (context) - Cartmell - 1990
12 Predicative type universes and primitive recursion (context) - Mendler - 1991
12 the interpretation of non-finitist proofs (context) - Kreisel - 1951
12 the interpretation of non-finitist proofs (context) - Kreisel - 1952
12 An intuitionistic theory of types: predicative part (context) - Martin-Lof - 1973
11 Infinitely long terms of transfinite type (context) - Tait - 1965
10 Routledge and Kegan Paul (context) - Wittgenstein - 1961
10 Inaccessibility in constructive set theory and type theory - Rathjen, or et al. - 1998
10 Structural recursive definitions in type theory - Gimenez - 1998
10 A finite axiomatization of inductive-recursive definitions - Dybjer, Setzer - 1999
9 The strength of some martin-lof type theories - or, Rathjen - 1994
8 Mendler-style inductive types (context) - Uustalu, Vene - 1999
8 Well-ordering proofs for martin-lof type theory with w-type .. (context) - Setzer - 1998
8 Ordinal analysis of terms of finite type (context) - Howard - 1980
8 Internal type theory - Dybjer - 1995
7 New version of the consistency proof for elementary number t.. (context) - Gentzen - 1969
7 A set constructor for inductive sets in martinl of's type th.. (context) - Petersson, Synek - 1989
7 London Mathematical Society monographs (context) - Conway, Games - 1976
6 Sets and Axioms: the apparatus of mathematics (context) - Hamilton - 1982
6 Clarendon Press (context) - Potter, An - 1990
6 Number 3 in Stockholm Studies in Philosophy (context) - Prawitz - 1965
6 An Introduction to the Theory of Surreal Numbers (context) - Gonshor - 1986
6 Beweistheoretische erfassung der unendliche induction in der.. (context) - Schutte - 1950
5 Cantorian set theory and Limitation of size (context) - Hallet - 1984
5 Oxford University Press (context) - Godel, Vol - 1990
5 The elements of mathematical logic (context) - Rosenbloom - 1950
5 Semantical Investigations into Intensional Type Theory (context) - Streicher - 1993
5 Functionals defined by recursion (context) - Sanchis - 1967
4 A construction of non-well-founded sets within martin-lof's .. (context) - Lindstrom - 1986
4 His Mathematics and Philosophy of the Infinite (context) - Dauben - 1979
4 Algorithmen fur ordnungszahlen und normalfunktionen (context) - Neumer - 1957
4 Algorithmen fur ordnungszahlen und normalfunktionen (context) - Neumer - 1960
4 Proofs as programs (context) - Schwichtenberg - 1992
4 the consistency of a certain logical calculus (context) - Novikov - 1943
3 Zur berechenbarkeit primitiv-recursiver functionale endliche.. (context) - Diller - 1970
3 The mathematical development of set theory from Cantor to Co.. - Kanamori - 1996
3 volume 42 of Synthese Library (context) - Stenlund, -Terms et al. - 1972
3 Bulletin of Symbolic Logic (context) - Pohlers, theory et al. - 1996
3 Hauptsatz for the intuitionistic theory of iterated inductiv.. (context) - Martin-Lof - 1971
3 The realm of ordinal analysis - Rathjen - 1997
3 Department of Computing Science (context) - Coquand, Type et al. - 1996
3 Describing ordinals using functionals of transfinite type (context) - Aczel - 1972
2 A first course in formal language theory (context) - Rayward-Smith - 1995
2 Well-ordering proofs in martin-lf's type theory (context) - Setzer - 1998
2 Extending martin-lf type theory by one mahlo-universe - Setzer - 1999
2 Half-ring morphologies (context) - Davis - 1967
2 Ordinals and ordinal functions representable in the simply t.. (context) - Danner - 1999
2 Relations between some hierarchies of Ordinal Functions and .. (context) - Weyrauch - 1972
2 Uber eine bisher noch nicht benutzte erwietung des finiten s.. (context) - Godel - 1958
2 Hereditarily replete functionals over the ordinals (context) - Feferman - 1968
2 Extensional Concepts in Extensional Type Theory (context) - Hofmann - 1995
2 A cube of proof systems for the intuitionistic predicate mu - Uustalu, Vene - 1997
2 chapter Notes on structured programming (context) - Dahl, Dijkstra et al. - 1971
2 The foundations of mathematics (context) - Hilbert - 1967
2 Die normalfunktionen und das problem der ausgezeichneten fol.. (context) - Bachmann - 1950
2 The strength of martin-lf type theory with a superuniverse (context) - Rathjen - 1999
2 Oldbourne Mathematical Series (context) - Rotman, Kneebone et al. - 1966
2 Number 48 in London Mathematical Society Student Texts (context) - Hahnal, Hamburger - 1999
2 Monadic presentations of lambda terms using generalized indu.. (context) - Alternkirch, Reus - 1999
2 Zur widerspruchsfreiheit det zahlentheorie (context) - Ackermann - 1940
2 Algebraische und logistische untersuchungen uber freie verba.. (context) - Lorenzen - 1951
2 Provability and nonprovability of restricted transfinite ind.. (context) - Gentzen - 1969
2 ein mathematische-philosophischer Versuch in der Lehre des U.. (context) - Cantor, allgemeinen
1 Mathematics of infinity (context) - Martin-Lof - 1990
1 Infinite terms and a system of natural deduction (context) - Martin-Lof - 1972
1 Regular ordinals and normal forms (context) - Isles - 1968
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.