Search results for "proofs-as-programs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
56	Jon Whittle 0001, Alan Bundy, Richard J. Boulton, Helen Lowe	An ML Editor Based on Proofs-As-Programs.	ASE	1999	DBLP DOI BibTeX RDF	proofs-as-programs, termination proof, Functional programming
38	James L. Caldwell	Moving Proofs-As-Programs into Practice.	ASE	1997	DBLP DOI BibTeX RDF	proofs-as-programs, constructive type theory, correct-by-construction programs, inductive proofs, Nuprl rewrite system, fixed-point combinators, untyped lambda calculus, specifications, partial evaluation, lambda calculus, hierarchical verifications
34	Iman Poernomo	Proofs-as-Imperative-Programs: Application to Synthesis of Contracts.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF
32	Iman Poernomo	Synthesis of Data Views for Communicating Processes.	LOPSTR	2007	DBLP DOI BibTeX RDF
25	Jon Whittle 0001, Alan Bundy, Richard J. Boulton	Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor.	Formal Aspects Comput.	2002	DBLP DOI BibTeX RDF	Programming environments, Functional programming, Theorem proving
21	Penny Anderson	Representing Proof Transformations for Program Optimizations.	CADE	1994	DBLP DOI BibTeX RDF
20	Iman Poernomo	Proofs-as-Model-Transformations.	ICMT@TOOLS	2008	DBLP DOI BibTeX RDF
18	Jane Hesketh, Alan Bundy, Alan Smaill	Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs.	CADE	1992	DBLP DOI BibTeX RDF
16	Ulrich Berger 0001	Proofs-as-Programs in Computable Analysis.	Electron. Commun. Eur. Assoc. Softw. Sci. Technol.	2009	DBLP DOI BibTeX RDF
16	Heidar Pirzadeh, Danny Dubé	Encoding the Program Correctness Proofs as Programs in PCC Technology.	PST	2008	DBLP DOI BibTeX RDF
16	Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley	Adapting Proofs-as-Programs - The Curry-Howard Protocol		2005	DOI RDF
16	Jonathan N. D. Whittle	The use of proofs-as-programs to build an analogy-based functional program editor.		1999	RDF
16	Michel Parigot	Classical Proofs as Programs.	Kurt Gödel Colloquium	1993	DBLP DOI BibTeX RDF
16	Chetan R. Murthy	Classical Proofs as Programs: How, What, and Why.	Constructivity in Computer Science	1991	DBLP DOI BibTeX RDF
16	Ulf R. Schmerl	A Cut-Elimination Procedure Designed for Evaluating Proofs as Programs.	CSL	1991	DBLP DOI BibTeX RDF
16	Joseph L. Bates, Robert L. Constable	Proofs as Programs.	ACM Trans. Program. Lang. Syst.	1985	DBLP DOI BibTeX RDF	PRL
16	Pierangelo Miglioli, Ugo Moscato, Mario Ornaghi	Constructive Proofs as Programs Executable by PrT Nets.	Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets	1981	DBLP DOI BibTeX RDF
14	David A. Basin	An Environment For Automated Reasoning About Partial Functions.	CADE	1988	DBLP DOI BibTeX RDF	Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions
13	Hiroshi Nakano	A Modality for Recursion.	LICS	2000	DBLP DOI BibTeX RDF	Lambda and Combinatory Caluculi, Type Systems and Type Theory, Specifications, Modal and Temporal Logics, Logics of Programs
12	Kazushige Terui	Light affine lambda calculus and polynomial time strong normalization.	Arch. Math. Log.	2007	DBLP DOI BibTeX RDF	Light logics, Lambda calculus, Polynomial time
7	Virgile Mogbil, Vincent Rahli	Uniform Circuits, & Boolean Proof Nets.	LFCS	2007	DBLP DOI BibTeX RDF
7	Peter Hines	Physical Systems as Constructive Logics.	UC	2006	DBLP DOI BibTeX RDF
7	Kazushige Terui	Proof Nets and Boolean Circuits.	LICS	2004	DBLP DOI BibTeX RDF
7	J. B. Wells, Boris Yakobowski	Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis.	LOPSTR	2004	DBLP DOI BibTeX RDF
7	Ichiro Ogata	A Proof Theoretical Account of Continuation Passing Style.	CSL	2002	DBLP DOI BibTeX RDF	Classical Natural Deduction, LKQ, classical proof theory, Classical Logic, CPS-translation, Call-By-Value
7	Frank Pfenning	On the Logical Foundations of Staged Computation (Abstract of Invited Talk).	PEPM	2000	DBLP DOI BibTeX RDF
7	Claudia Faggian	Classical Proofs via Basic Logic.	CSL	1997	DBLP DOI BibTeX RDF