Search results for "proof-terms"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
48	Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002	Proof Search and Proof Check for Equational and Inductive Theorems.	CADE	2003	DBLP DOI BibTeX RDF	proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant
35	Ruy J. G. B. de Queiroz	On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics.	Stud Logica	2008	DBLP DOI BibTeX RDF	reduction rules, proof-terms, proof-theoretic semantics, game-theoretic semantics, dialogue semantics, natural deduction
26	Stefan Berghofer, Tobias Nipkow	Proof Terms for Simply Typed Higher Order Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
18	Juan Chen 0002, Ravi Chugh, Nikhil Swamy	Type-preserving compilation of end-to-end verification of security enforcement.	PLDI	2010	DBLP DOI BibTeX RDF	bytecode languages, compilers, authorization, functional programming, information flow, dependent types, security type systems, mobile code security
18	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
18	Masami Hagiya	Programming by Example and Proving by Example Using Higher-order Unification.	CADE	1990	DBLP DOI BibTeX RDF
17	Yuta Takahashi, Ryo Takemura	Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms.	J. Philos. Log.	2019	DBLP DOI BibTeX RDF
17	Christina Kohl, Aart Middeldorp	Composing Proof Terms.	CADE	2019	DBLP DOI BibTeX RDF
17	Gabriel Ebner	Fast Cut-Elimination using Proof Terms: An Empirical Study.	CL&C	2018	DBLP DOI BibTeX RDF
17	Franck Slama	Automatic generation of proof terms in dependently typed programming languages.		2018	RDF
17	Herman Geuvers, Tonny Hurkens	Proof Terms for Generalized Natural Deduction.	TYPES	2017	DBLP DOI BibTeX RDF
17	José Espírito Santo, Maria João Frade, Luís Pinto 0001	Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts.	TYPES	2016	DBLP DOI BibTeX RDF
17	Carlos Lombardi, Alejandro Ríos 0001, Roel de Vrijer	Proof terms for infinitary rewriting, progress report.	CoRR	2014	DBLP BibTeX RDF
17	Carlos Lombardi, Alejandro Ríos 0001, Roel de Vrijer	Proof Terms for Infinitary Rewriting.	RTA-TLCA	2014	DBLP DOI BibTeX RDF
17	Ferruccio Guidi	Procedural Representation of CIC Proof Terms.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
17	Claudio Sacerdoti Coen	Declarative Representation of Proof Terms.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
17	Mitsuhiro Okada, Ryo Takemura	Remarks on Semantic Completeness for Proof-Terms with Laird's Dual Affine/Intuitionistic lambda -Calculus.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
17	Eike Ritter, David J. Pym, Lincoln A. Wallen	Proof-terms for classical and intuitionistic resolution.	J. Log. Comput.	2000	DBLP DOI BibTeX RDF
17	Ken-etsu Fujita	On Proof Terms and Embeddings of Classical Substructural Logics.	Stud Logica	1998	DBLP DOI BibTeX RDF
17	Eike Ritter, David J. Pym, Lincoln A. Wallen	Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract).	CADE	1996	DBLP DOI BibTeX RDF
17	Benjamin Grégoire, Jorge Luis Sacchini	Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.	TGC	2007	DBLP DOI BibTeX RDF
17	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
17	Evan Goris	Explicit Proofs in Formal Provability Logic.	LFCS	2007	DBLP DOI BibTeX RDF
14	Guillaume Melquiond	Proving Bounds on Real-Valued Functions with Computations.	IJCAR	2008	DBLP DOI BibTeX RDF
14	Olivier Boite	Proof Reuse with Extended Inductive Types.	TPHOLs	2004	DBLP DOI BibTeX RDF
14	Alexandre Miquel, Benjamin Werner	The Not So Simple Proof-Irrelevant Model of CC.	TYPES	2002	DBLP DOI BibTeX RDF
14	Marko Luther	More On Implicit Syntax.	IJCAR	2001	DBLP DOI BibTeX RDF
11	Richard Bonichon, David Delahaye, Damien Doligez	Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.	LPAR	2007	DBLP DOI BibTeX RDF
11	Alexandre Miquel	Classical Program Extraction in the Calculus of Constructions.	CSL	2007	DBLP DOI BibTeX RDF
11	Bruno Barras, Benjamin Grégoire	On the Role of Type Decorations in the Calculus of Inductive Constructions.	CSL	2005	DBLP DOI BibTeX RDF
11	Claudio Sacerdoti Coen	Explanation in Natural Language of lamda-µµ-Terms.	MKM	2005	DBLP DOI BibTeX RDF
11	Einar Broch Johnsen, Christoph Lüth	Theorem Reuse by Proof Term Transformation.	TPHOLs	2004	DBLP DOI BibTeX RDF
8	Peter W. O'Hearn	Resource Interpretations, Bunched Implications and the alpha lambda-Calculus.	TLCA	1999	DBLP DOI BibTeX RDF
8	José Meseguer 0001, Carolyn L. Talcott	A Partial Order Event Model for Concurrent Objects.	CONCUR	1999	DBLP DOI BibTeX RDF
8	Shenwei Yu, Zhaohui Luo	Implementing a Model Checker for LEGO.	FME	1997	DBLP DOI BibTeX RDF
8	Kentaro Kikuchi, Stéphane Lengrand	Strong Normalisation of Cut-Elimination That Simulates beta-Reduction.	FoSSaCS	2008	DBLP DOI BibTeX RDF
8	Tobias Nipkow	Higher-Order Rewrite Systems (Abstract).	RTA	1995	DBLP DOI BibTeX RDF
5	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
5	Anna Zamansky, Nissim Francez, Yoad Winter	A 'Natural Logic' inference system using the Lambek calculus.	J. Log. Lang. Inf.	2006	DBLP DOI BibTeX RDF	Natural logic, Inference, Normalization, Lambek calculus
5	Limin Jia 0001, David Walker 0001	Modal Proofs as Distributed Programs (Extended Abstract).	ESOP	2004	DBLP DOI BibTeX RDF
5	H. J. Sander Bruggink	Residuals in Higher-Order Rewriting.	RTA	2003	DBLP DOI BibTeX RDF
5	Aleksandar Nanevski	Meta-programming with names and necessity.	ICFP	2002	DBLP DOI BibTeX RDF	modal lambda-calculus, higher-order abstract syntax