Christoph Kreitz  @ NUS Home/Search
Context Related
| cornell.edu/Info/People/kr...96igpl.ps cornell.edu/home/kreitz/PS...96igpl.ps dcs.kcl.ac.uk/journals/I...kreitz.ps.gz Cached: PS.gz PS PDF Image Update Help From: cornell.edu/Info/People/...papers (more) From: cornell.edu/home/kreitz/papers (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: We describe a formalization of the meta-mathematics of programming in a higher-order logical calculus as a means to create verifiably correct implementations of program synthesis tools. Using reflected notions of programming concepts we can specify the actions of synthesis methods within the object language of the calculus and prove formal theorems about their behavior. The theorems serve as derived inference rules implementing the kernel of these methods in a flexible, safe, efficient and... (Update)
Context of citations to this paper: More
.... synthesis from low level calculi to one comprehensible for programmers and to implement program development strategies on this level [Kre96]. These are considered to be steps on the way towards enabling a user of a program development system to focus on the key ideas in...
...etc. has been extremely successful during the period of the last three years as can be seen from the selected list of publications [5, 38, 39, 40]. This work has brought theorem proving techniques closer to system development practice and altogether resulted in the system...
Cited by: More
A Multi-level Approach to Program Synthesis - Bibel, Korn, Kreitz, Kurucz.. (1997) (Correct)
Matrix-based Constructive Theorem Proving - Kreitz, Otten, Schmitt, Pientka (1999) (Correct)
A Proof Environment for the Development of Group.. - Kreitz, Hayden, Hickey (1998) (Correct)
Active bibliography (related documents): More All
1.3: Towards a formal Theory of Program Construction - Kreitz (1990) (Correct)
0.6: Logic Program Synthesis - Deville, Lau (1993) (Correct)
0.5: Guiding Program Development Systems by a Connection Based .. - Kreitz, Otten, Schmitt (1996) (Correct)
Similar documents based on text: More All
0.3: Connection-based Theorem Proving in Classical and.. - Kreitz, Otten (1999) (Correct)
0.2: On Transforming Intuitionistic Matrix Proofs into.. - Stephan Schmitt.. (1995) (Correct)
0.2: Spatial Reasoning and Connectionist Inference - Beringer, Hölldobler, Kurfeß (1993) (Correct)
Related documents from co-citation: More All
6: Implementing Mathematics with the Nuprl Proof Development System - Constable - 1986
6: Guiding Program Development Systems by a Connection Based Proof Strategy - Kreitz, Otten et al. - 1996
5: ACM Transactions on Programming Languages and Systems (context) - Bates, Constable et al. - 1985
BibTeX entry: (Update)
C. Kreitz. Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4(1):75--94, 1996. http://citeseer.comp.nus.edu.sg/115832.html More
@misc{ kreitz96formal,
author = "C. Kreitz",
title = "Formal mathematics for verifiably correct program synthesis",
text = "C. Kreitz. Formal mathematics for verifiably correct program synthesis.
Journal of the IGPL, 4(1):75--94, 1996.",
year = "1996",
url = "citeseer.comp.nus.edu.sg/115832.html" }
Citations (may not include all citations):505 Implementing Mathematics with the NuPRL proof development sy.. - Constable - 1986
266 Information and Computation (context) - Coquand, Huet et al. - 1988
163 An application of theorem proving to problem solving (context) - Green - 1969
150 Edinburgh LCF: A mechanized Logic of Computation (context) - Gordon, Milner et al. - 1979
145 Isabelle: The next 700 theorem provers (context) - Paulson - 1990
129 The foundation of a generic theorem prover - Paulson - 1989
128 Logic and Computation: Interactive Proof with Cambridge LCF (context) - Paulson - 1987
94 A deductive approach to program synthesis (context) - Manna, Waldinger - 1980
67 KIDS --- a knowledge-based software development system - Smith - 1991
53 The semantics of reflected proof - Allen, Constable et al. - 1990
42 Top-down synthesis of divide-and-conquer algorithms (context) - Smith - 1985
40 Science of Computer Programming (context) - Smith, Lowry et al. - 1990
37 Tactical theorem proving in program verification (context) - Heisel, Reif et al. - 1990
29 Proofs and Types (context) - Girard, Lafont et al. - 1989
21 Formalized metareasoning in Type Theory (context) - Knoblock, Constable - 1986
15 IEEE Transactions on Software Engineering (context) - Manna, Waldinger et al. - 1979
12 semantics--supported program synthesis (context) - Bibel - 1980
10 Studies in Proof Theory Lecture Notes (context) - Martin-Lof, Theory - 1984
7 METASYNTHESIS: Deriving Programs that Develop Programs (context) - Kreitz - 1993
5 The Extraction and Optimization of Programs from Constructiv.. (context) - Sasaki - 1985
4 Metamathematical extensibility in Type Theory (context) - Knoblock - 1987
3 PX: a system extracting programs from proofs (context) - Hayashi - 1986
2 A study of a class of detection waveforms having nearly idea.. (context) - Costas - 1984
2 Towards a formal theory of program construction - Kreitz - 1990
2 XPRTS - an implementation tool for program synthesis (context) - Neugebauer, Fronhofer et al. - 1989
2 The theory of LEGO -- a proof checker for the extendend calc.. (context) - Pollack - 1994
2 Automatic guidance of program synthesis proofs (context) - Bundy - 1989
The graph only includes citing articles where the year of publication is known.
Documents on the same site (http://simon.cs.cornell.edu/Info/People/kreitz/papers.html): More
A Uniform Proof Procedure for Classical and Non-Classical Logics - Otten, Kreitz (1996) (Correct)
Converting Non-Classical Matrix Proofs into Sequent-Style.. - Schmitt, Kreitz (1996) (Correct)
Connection-based Theorem Proving in Classical and.. - Christoph Kreitz.. (1999) (Correct)
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.