Search results for "Proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
28	Isabel Oitavem	Implicit Characterizations of Pspace.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	implicit characterizations, computational complexity, term rewriting, Pspace
28	Matthias Baaz, Alexander Leitsch	Comparing the Complexity of Cut-Elimination Methods.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
28	Gordon D. Plotkin, Colin Stirling, Mads Tofte (eds.)	Proof, Language, and Interaction, Essays in Honour of Robin Milner	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Didier Galmiche (eds.)	Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics 2000, held in conjunction with CADE-17 Conference, Pittsburgh, PA, USA, June 20-21, 2000	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP BibTeX RDF
28	Gordon D. Plotkin, Colin Stirling, Mads Tofte	A brief scientific biography of Robin Milner.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	C. A. R. Hoare, Jifeng He 0001, Augusto Sampaio	Algebraic derivation of an operational semantics.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Pierre-Louis Curien, Gordon D. Plotkin, Glynn Winskel	Bistructures, bidomains, and linear logic.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Gérard P. Huet, Amokrane Saïbi	Constructive category theory.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Jaco de Bakker, Franck van Breugel	From Banach to Milner: metric semantics for second order communication and concurrency.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Gérard Boudol, Cosimo Laneve	lambda-calculus, multiplicities, and the pi-calculus.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Davide Sangiorgi	Lazy functions and mobile processes.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Robert Harper 0001, Christopher A. Stone	A type-theoretic interpretation of standard ML.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Sergey Berezin, Edmund M. Clarke, Somesh Jha, Will Marrero	Model checking algorithms for the µ-calculus.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Joachim Parrow	Trios in concert.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	William Ferreira 0001, Matthew Hennessy, Alan Jeffrey	Combining the typed lambda-calculus with CCS.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Yoram Hirshfeld, Faron Moller	On the star height of unary regular behaviours.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe	Constructively formalizing automata theory.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Fabio Gadducci, Ugo Montanari	The tile model.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Mike Gordon	From LCF to HOL: a short history.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Gérard Berry	The foundations of Esterel.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Uffe Engberg, Mogens Nielsen	A calculus of communicating systems with label passing - ten years after.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Xinxin Liu 0008, David Walker 0008	Concurrent objects as mobile processes.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Eugene W. Stark, Scott A. Smolka	A complete axiom system for finite-state probabilistic processes.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Benjamin C. Pierce, David N. Turner	Pict: a programming language based on the Pi-Calculus.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Samson Abramsky	Axioms for definability and full completeness.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Jos C. M. Baeten, Jan A. Bergstra, Michel A. Reniers	Discrete time process algebra with silent step.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Lawrence C. Paulson	A fixedpoint approach to (co)inductive and (co)datatype definitions.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Pierre Collette, Cliff B. Jones	Enhancing the tractability of rely/guarantee specifications in the development of interfering operations.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Mads Tofte, Lars Birkedal	Unification and polymorphism in region inference.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
28	Aleksey Nogin	Writing Constructive Proofs Yielding Efficient Extracted Programs.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
28	Didier Galmiche	Preface.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
28	James Harland, David J. Pym, Michael Winikoff	Forward and Backward Chaining in Linear Logic.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
28	Ernst W. Mayr, Hans Jürgen Prömel, Angelika Steger (eds.)	Lectures on Proof Verification and Approximation Algorithms. (the book grow out of a Dagstuhl Seminar, April 21-25, 1997)	Lectures on Proof Verification and Approximation Algorithms	1998	DBLP DOI BibTeX RDF
28	Paul Beame, Samuel R. Buss (eds.)	Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996	Proof Complexity and Feasible Arithmetics	1998	DBLP DOI BibTeX RDF
28	Didier Galmiche (eds.)	Workshop on Proof Search in Type-Theoretic Languages (in conjunction with CADE-15 Conference), Lindau, Germany, July 5, 1998	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP BibTeX RDF
28	Paul Mukherjee, John S. Fitzgerald	The Ammunition Control System.	Proof in VDM	1998	DBLP DOI BibTeX RDF
28	Noemie Slaats, Bart Van Assche, Albert Hoogewijs	Shared Memory Synchronization.	Proof in VDM	1998	DBLP DOI BibTeX RDF
28	Sten Agerholm, Juan Bicarregui, Savi Maharaj	On the Verification of VDM Specification and Refinement with PVS.	Proof in VDM	1998	DBLP DOI BibTeX RDF
28	Peter Lindsay	Specification and Validation of a Network Security Policy Model.	Proof in VDM	1998	DBLP DOI BibTeX RDF
28	David J. Pym	Logic Programming with Bunched Implications.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Michael Franssen	Embedding First-Order Tableaux into a Pure Type System.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Frank Pfenning, Carsten Schürmann	Algorithms for Equality and Unification in the Presence of Notational Definitions.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Didier Galmiche	Preface.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Luís Pinto 0001, Roy Dyckhoff	Sequent Calculi for the Normal Terms of the - and - Calculi.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Dominique Larchey-Wendling, Didier Galmiche	Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
28	Sebastian Seibert, Thomas Wilke	Bounds for Approximating MAXLINEQ3-2 and MAXEKSAT.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Thomas Jansen 0001	Introduction to the Theory of Complexity and Approximation Algorithms.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Martin Mundhenk, Anna Slobodová	Optimal Non-approximability of MAXCLIQUE.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Katja Wolf	Dense Instances of Hard Optimization Problems.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Thomas Hofmeister, Martin Hühne	Semidefinite Programming and Its Applications to Approximation Algorithms.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Artur Andrzejak 0001	Introduction to Randomized Algorithms.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Claus Rick, Hein Röhrig	Deriving Non-approximability Results by Reductions.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Detlef Sieling	Derandomization.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
28	Peter Clote, Anton Setzer	On PHP st-connectivity, and odd charged graphs.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Samuel R. Buss	Lower bounds on Nullstellensatz proofs via designs.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Paul Beame, Søren Riis	More on the relative strength of counting principles.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	François Pitt	A quantifier-free theory based on a string algebra for NC1.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Alexis Maciel, Toniann Pitassi	Towards lower bounds for bounded-depth Frege proofs with modular connectives.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Jeremy Avigad	Plausibly hard combinatorial tautologies.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Rodney G. Downey, Michael R. Fellows, Kenneth W. Regan	Descriptive complexity and the W hierarchy.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Stephen Cook	Relating the provable collapse of P to NC1 and the power of logical theories.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Dan E. Willard	Self-reflection principles and NP-hardness.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Stasys Jukna	Exponential lower bounds for semantic resolution.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Jan Johannsen	Equational calculi and constant depth propositional proofs.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Xudong Fu	Lower bounds on sizes of cutting plane proofs for modular coloring principles.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Barbara Kauffmann	Bounded arithmetic: Comparison of Buss' witnessing method and Sieg's Herbrand analysis.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Stephen J. Bellantoni	Ranking arithmetic proofs by implicit ramification.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
28	Roy Dyckhoff, Lars-Henrik Eriksson, Alberto Momigliano, Mario Ornaghi (eds.)	ICLP 1994, Workshop W10: Proof-Theoretical Extensions on Logic Programming, Santa Margherita Ligure, Italy, June 1994	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Per Kreuger	A-Sufficient Substitutions in mixed Contents.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Lars Hallnäs, Per Kreuger	Partial Inductive Definitions (Tutorial).	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Peter J. Robinson 0001, John Staples, Anthony S. K. Cheng	Theorem Proving Applications for QU-Prolog.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Didier Galmiche	Canonical Proofs for Linear Logic Programming Frameworks.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Jonas Barklund, Stefania Costantini, Pierangelo Dell'Acqua, Gaetano Aurelio Lanzarone	Integrating Reflection into SLD-Resolution.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	I. Stephan	An SLOU Prolog Interpreter.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Göran Falkman, Lars Hallnäs, Olof Torgersson	Program Separation in GCLA.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Francesca Arcelli, Ferrante Formato	Higher-Order Implementation of Program Transformations using Algebraic Specification.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Matteo Baldoni, Laura Giordano 0001, Alberto Martelli	A Modal Extension of Logic Programming.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	R. S. Kemp, Graem A. Ringwood	Reynold and Heyling Models of Logic Programs.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Roy Dyckhoff, Luís Pinto 0001	Uniform Proofs and Natural Deduction.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Iliano Cervesato	Lollipops Taste of Vanilla too.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
28	Alberto Coen-Porisini, Richard A. Kemmerer, Dino Mandrioli	A Formal Framework for ASTRAL Intralevel Proof Obligations.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	intralevel proof obligations, formal software development, mathematical correctness, ASLAN, TRIO, real-time systems, real-time systems, verification, formal specification, formal specification, formal methods, finite state machines, program verification, specification languages, state machines, formal specification language, formal proof, timing requirements, ASTRAL
28	A. Wolinsky	A simple proof of Lewin's ordered-retrieval theorem for associative memories.	Commun. ACM	1968	DBLP DOI BibTeX RDF	access frequency proof, column digit values, column sensing arrangement, digit value readout, digit value variety, digit variety readout, memory access frequency, ordered information retrieval, ordered lists, ordered retrieval efficiency, ordered retrieval theorem, retrieval theorem proof, associative memories, content-addressed memories, memory access
27	Paul Valiant	Incrementally Verifiable Computation or Proofs of Knowledge Imply Time/Space Efficiency.	TCC	2008	DBLP DOI BibTeX RDF
27	Chuck C. Liang, Dale Miller 0001	Focusing and Polarization in Intuitionistic Logic.	CSL	2007	DBLP DOI BibTeX RDF
27	Ralph D. Jeffords, Constance L. Heitmeyer	A strategy for efficiently verifying requirements.	ESEC / SIGSOFT FSE	2003	DBLP DOI BibTeX RDF	model checking, formal methods, software tools, invariants, requirements specification, compositional verification
27	Bruce Spencer, Joseph Douglas Horton	Support Ordered Resolution.	CADE	2000	DBLP DOI BibTeX RDF
27	Peter B. Andrews	Transforming Matings into Natural Deduction Proofs.	CADE	1980	DBLP DOI BibTeX RDF
27	Reynald Affeldt, Miki Tanaka, Nicolas Marti	Formal Proof of Provable Security by Game-Playing in a Proof Assistant.	ProvSec	2007	DBLP DOI BibTeX RDF
27	Julian Richardson	A Semantics for Proof Plans with Applications to Interactive Proof Planning.	LPAR	2002	DBLP DOI BibTeX RDF
27	Marco Meoni	Interactive Parallel Analysis on the ALICE Grid with the PROOF Framework.	ICCS (1)	2009	DBLP DOI BibTeX RDF	interactive parallel distributed processing, task colocation, Grid, PROOF, ALICE, resource availability, data movement
27	Kriangsak Damchoom, Michael J. Butler, Jean-Raymond Abrial	Modelling and Proof of a Tree-Structured File System in Event-B and Rodin.	ICFEM	2008	DBLP DOI BibTeX RDF	Rodin tool, Refinement, File system, Tree structure, Proof, Event-B
27	Olivier Laurent 0001, Roberto Maieli	Cut Elimination for Monomial MALL Proof Nets.	LICS	2008	DBLP DOI BibTeX RDF	Linear Logic, Cut Elimination, Proof Net
27	Hirohiko Kushida, Mitsu Okada	A proof-theoretic study of the correspondence of hybrid logic and classical logic.	J. Log. Lang. Inf.	2007	DBLP DOI BibTeX RDF	Proof theory, Hybrid logic, Classical logic
27	Andrzej S. Murawski, C.-H. Luke Ong	Fast verification of MLL proof nets via IMLL.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	Multiplicative linear logic, disjoint union find, essential nets, dominator trees, proof nets
27	Zhicheng Wen, Huaikou Miao, Hongwei Zeng	Generating Proof Obligation to Verify Object-Z Specification.	ICSEA	2006	DBLP DOI BibTeX RDF	formal specification, Object-Z, proof obligation
27	Stefano Baratella, Andrea Masini	An approach to infinitary temporal proof theory.	Arch. Math. Log.	2004	DBLP DOI BibTeX RDF	Modal logic, Proof theory, Sequent calculus, Cut elimination, Infinitary logic
27	Masahiro Hamano	Softness of MALL proof-structures and a correctness criterion with Mix.	Arch. Math. Log.	2004	DBLP DOI BibTeX RDF	Multiplicative Additive Proof-Nets, Linear Logic, Sequentialization
27	Kazuhiro Ogata 0001, Kokichi Futatsugi	Proof Scores in the OTS/CafeOBJ Method.	FMOODS	2003	DBLP DOI BibTeX RDF	observational transition system, proof scores, the NSLPK authentication protocol, verification, Algebraic specification, CafeOBJ
27	Kenji Terada, Makoto Yokoo	False-name-proof multi-unit auction protocol utilizing greedy allocation based on approximate evaluation values.	AAMAS	2003	DBLP DOI BibTeX RDF	false-name-proof, multi-unit auction, mechanism design
27	Andrew Bernard, Peter Lee 0001	Temporal Logic for Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF	temporal logic, Proof-carrying code