Search results for "proofs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
29	Serge Autexier, Claudio Sacerdoti Coen	A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus.	MKM	2006	DBLP DOI BibTeX RDF
29	Véronique Cortier, Bogdan Warinschi	Computationally Sound, Automated Proofs for Security Protocols.	ESOP	2005	DBLP DOI BibTeX RDF
29	Kim-Kwang Raymond Choo, Colin Boyd, Yvonne Hitchcock	Errors in Computational Complexity Proofs for Protocols.	ASIACRYPT	2005	DBLP DOI BibTeX RDF
29	Cristian Calude, Solomon Marcus	Mathematical Proofs at a Crossroad?	Theory Is Forever	2004	DBLP DOI BibTeX RDF
29	Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer 0001	Certifying and Synthesizing Membership Equational Proofs.	FME	2003	DBLP DOI BibTeX RDF
29	Sunae Seo, Hongseok Yang, Kwangkeun Yi	Automatic Construction of Hoare Proofs from Abstract Interpretation Results.	APLAS	2003	DBLP DOI BibTeX RDF
29	Michael Backes 0001, Matthias Schunter	From absence of certain vulnerabilities towards security proofs: pushing the limits of formal verification.	NSPW	2003	DBLP DOI BibTeX RDF	formal methods, cryptography
29	Herman Geuvers, Gueorgui I. Jojgov	Open Proofs and Open Terms: A Basis for Interactive Logic.	CSL	2002	DBLP DOI BibTeX RDF	open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving
29	Sofie Verbaeten, Danny De Schreye, Konstantinos Sagonas	Termination proofs for logic programs with tabling.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	prolog, tabling, SLG-resolution
29	Eli Ben-Sasson, Avi Wigderson	Short proofs are narrow - resolution made simple.	J. ACM	2001	DBLP DOI BibTeX RDF
29	Georg Struth	Calculating Church-Rosser Proofs in Kleene Algebra.	RelMiCS	2001	DBLP DOI BibTeX RDF	$lambda$-calculus, Church-Rosser theorem, rewriting, Kleene algebra, formal mathematics
29	Mike Burmester, Yvo Desmedt, Toshiya Itoh, Kouichi Sakurai, Hiroki Shizuya	Divertible and Subliminal-Free Zero-Knowledge Proofs for Languages.	J. Cryptol.	1999	DBLP DOI BibTeX RDF	Divertibility, Subliminal-free, Cryptographic protocols, Identification, Zero-knowledge, Proof systems, Untraceability
29	Michael T. Goodrich, Roberto Tamassia	Teaching the analysis of algorithms with visual proofs.	SIGCSE	1998	DBLP DOI BibTeX RDF
29	Hans-Jörg Tiede	Lambek Calculus Proofs and Tree Automata.	LACL	1998	DBLP DOI BibTeX RDF
29	Thierry Coquand, Henrik Persson	Gröbner Bases in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF
29	Yann Coscoy	A Natural Language Explanation for Formal Proofs.	LACL	1996	DBLP DOI BibTeX RDF
29	Wai Wong	Recording and Checking HOL Proofs.	TPHOLs	1995	DBLP DOI BibTeX RDF
29	Alfredo De Santis, Tatsuaki Okamoto, Giuseppe Persiano	Zero-Knowledge Proofs of Computational Power in the Shared String Model.	ASIACRYPT	1994	DBLP DOI BibTeX RDF
29	Kurt Ammon	Automatic Proofs in Mathematical Logic and Analysis.	CADE	1992	DBLP DOI BibTeX RDF
29	Tatsuaki Okamoto	An Extensin of Zero-Knowledge Proofs and Its Applications.	ASIACRYPT	1991	DBLP DOI BibTeX RDF
29	Mike Burmester, Yvo Desmedt	Broadcast Interactive Proofs (Extended Abstract).	EUROCRYPT	1991	DBLP DOI BibTeX RDF
29	Wu-Tung Cheng, Janak H. Patel	PROOFS: a super fast fault simulator for sequential circuits.	EURO-DAC	1990	DBLP DOI BibTeX RDF
29	Thomas M. Niermann, Wu-Tung Cheng, Janak H. Patel	Proofs: A Fast, Memory Efficient Sequential Circuit Fault Simulator.	DAC	1990	DBLP DOI BibTeX RDF
29	Peter B. Andrews	Transforming Matings into Natural Deduction Proofs.	CADE	1980	DBLP DOI BibTeX RDF
28	Roman Kuznets	Proof Identity for Classical Logic: Generalizing to Normality.	LFCS	2007	DBLP DOI BibTeX RDF
28	Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene	Using TAME to prove invariants of automata models: Two case studies.	FMSP	2000	DBLP DOI BibTeX RDF	software requirements analysis, Software engineering, verification, formal methods, theorem proving
28	John N. Crossley	Practical Logic (Abstract).	ISAAC	1995	DBLP DOI BibTeX RDF
28	Mihir Bellare, Chanathip Namprempre, Gregory Neven	Security Proofs for Identity-Based Identification and Signature Schemes.	J. Cryptol.	2009	DBLP DOI BibTeX RDF	Signatures, Identity-based cryptography, Identification schemes, Security proofs
28	Dorota Leszczynska-Jasion	The Method of Socratic Proofs for Modal Propositional Logics: K5, S4.2, S4.3, S4F, S4R, S4M and G.	Stud Logica	2008	DBLP DOI BibTeX RDF	modal propositional logics, extensions of logic S4, the method of Socratic proofs, logic of questions, Inferential EroteticLogic
28	Julia Kempe, Hirotada Kobayashi, Keiji Matsumoto, Thomas Vidick	Using Entanglement in Quantum Multi-prover Interactive Proofs.	CCC	2008	DBLP DOI BibTeX RDF	quantum interactive proofs, public-coin, parallelization, entanglement
28	Juan Manuel Crespo, Gustavo Betarte, Carlos Luna 0001	A Framework for the Analysis of Access Control Models for Interactive Mobile Devices.	TYPES	2008	DBLP DOI BibTeX RDF	mobile devices, Access control models, formal proofs
28	Yvonne Hitchcock, Colin Boyd, Juan Manuel González Nieto	Modular proofs for key exchange: rigorous optimizations in the Canetti-Krawczyk model.	Appl. Algebra Eng. Commun. Comput.	2006	DBLP DOI BibTeX RDF	Canetti, Krawczyk model, Security proofs, Key exchange protocols
28	Ulrich Berger 0001, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg	Program Extraction from Normalization Proofs.	Stud Logica	2006	DBLP DOI BibTeX RDF	Normalization by evaluation, program extraction from proofs, realizability, typed lambda calculus
28	Martin Sulzmann	Extracting programs from type class proofs.	PPDP	2006	DBLP DOI BibTeX RDF	proofs are programs principle, overloading, type classes
28	Andrzej Wisniewski, Guido Vanackere, Dorota Leszczynska	Socratic Proofs and Paraconsistency: A Case Study.	Stud Logica	2005	DBLP DOI BibTeX RDF	Socratic proofs, logic of questions, paraconsistent logics
28	Kumar Chellapilla, Kevin Larson, Patrice Y. Simard, Mary Czerwinski	Designing human friendly human interaction proofs (HIPs).	CHI	2005	DBLP DOI BibTeX RDF	completely automated public turing tests to tell computers and humans apart (CAPTCHAs), visual letter recognition, evaluation, computer vision, human perception, human interaction proofs (HIPs)
28	Idit Keidar, Roger Khazan, Nancy A. Lynch, Alexander A. Shvartsman	An inheritance-based technique for building simulation proofs incrementally.	ACM Trans. Softw. Eng. Methodol.	2002	DBLP DOI BibTeX RDF	Inheritance by specialization and subclassing for extension, incremental proof techniques, proof reuse, simulation proofs, refinements
28	Dima Grigoriev	Complexity of Positivstellensatz proofs for the knapsack.	Comput. Complex.	2001	DBLP DOI BibTeX RDF	Polynomial calculus, Positivstellensatz proofs, complexity of the knapsack
28	Dima Grigoriev	Tseitin's Tautologies and Lower Bounds for Nullstellensatz Proofs.	FOCS	1998	DBLP DOI BibTeX RDF	Nullstellensatz proofs, Tseitin's tautologies, lower bounds, expander
28	Lawrence C. Paulson	Mechanized proofs for a recursive authentication protocol.	CSFW	1997	DBLP DOI BibTeX RDF	mechanized proofs, recursive authentication protocol, inductive approach, message nesting, basic security theorem, adjacent pairs, honest agents, protocol complexity, agents, protocols, specification, symmetry, mutual authentication, Isabelle/HOL, session keys
28	Maria Luisa Bonet, Toniann Pitassi, Ran Raz	No Feasible Interpolation for TC0-Frege Proofs.	FOCS	1997	DBLP DOI BibTeX RDF	TC/sup 0/-Frege proofs, feasible interpolation, complexity-theoretic assumption, hardness assumption, lower bounds, theorem proving, Chinese Remainder Theorem, proof systems
28	Steven Parkes, Prithviraj Banerjee, Janak H. Patel	A parallel algorithm for fault simulation based on PROOFS .	ICCD	1995	DBLP DOI BibTeX RDF	fault partitioning, dynamic partitioning schemes, compute intensive task, integrated circuit design process, rapid design turn around, ProperPROOFS, parallel extension, PROOFS fault simulation package, distributed method, fault redistribution, ISCAS-89 benchmark set, high performance serial fault simulation applications, parallel algorithms, parallel algorithm, parallel architectures, parallel architectures, fault diagnosis, logic testing, sequential circuits, sequential circuits, circuit analysis computing, logic partitioning
28	Paolo Volpe	Concurrent Logic Programming as Uniform Linear Proofs.	ALP	1994	DBLP DOI BibTeX RDF	Uniform Proofs, Phase Semantics, Chemical Abstract Machine, Concurrency, Linear Logic
28	Bertram Fronhöfer	Linear Proofs and Linear Logic.	JELIA	1992	DBLP DOI BibTeX RDF	Linear Proofs, Logics for Planning, Linear Logic
28	Alan Bundy	The Use of Explicit Plans to Guide Inductive Proofs.	CADE	1988	DBLP DOI BibTeX RDF	inductive proofs, formal methods, planning, theorem proving, automatic programming, Proof plans
27	Jung-Min Park 0001, Edwin K. P. Chong, Howard Jay Siegel	Constructing fair-exchange protocols for E-commerce via distributed computation of RSA signatures.	PODC	2003	DBLP DOI BibTeX RDF	e-commerce, zero-knowledge proofs, multisignatures, RSA signatures, Fair-exchange protocols
27	Maria Luisa Bonet, Nicola Galesi	Optimality of size-width tradeoffs for resolution.	Comput. Complex.	2001	DBLP DOI BibTeX RDF	complexity of proofs, automated theorem proving.¶ Subject classification. 03F20, 03B05, Resolution, 68T15
27	Satoshi Hada, Toshiaki Tanaka	A Relationship between One-Wayness and Correlation Intractability.	Public Key Cryptography	1999	DBLP DOI BibTeX RDF	correlation intractability, zero-knowledge, One-way functions, random oracle, interactive proofs, round complexity
27	Ran Raz	Quantum Information and the PCP Theorem.	Algorithmica	2009	DBLP DOI BibTeX RDF	Quantum interactive proofs, Quantum advice, Quantum computation, Probabilistically checkable proofs, Quantum information, Low degree test
27	Adi Shamir	IP=PSPACE	FOCS	1990	DBLP DOI BibTeX RDF	acceptance probability, honest provers, public coins, logarithmic workspace, two-way access, random tape, interaction, IP, randomization, polynomial time, one-way functions, zero-knowledge proofs, interactive proofs, PSPACE, polynomial space, proof verification
25	John Wickerson	Ribbon Proofs.	Arch. Formal Proofs	2013	DBLP BibTeX RDF
25	B. Malcolm Brown, Erich L. Kaltofen, Shin'ichi Oishi, Siegfried M. Rump (eds.)	Computer-assisted proofs - tools, methods and applications, 15.11. - 20.11.2009	Computer-assisted proofs - tools, methods and applications	2009	DBLP BibTeX RDF
25	Andreas Rauh, Ekaterina Auer	Interval Approaches to Reliable Control of Dynamical Systems.	Computer-assisted proofs - tools, methods and applications	2009	DBLP BibTeX RDF
25	Ekaterina Auer, Roger Cuypers, Eva Dyllong, Stefan Kiel, Wolfram Luther	Verification and Validation for Femur Prosthesis Surgery.	Computer-assisted proofs - tools, methods and applications	2009	DBLP BibTeX RDF
25	Bruno Buchberger, Shin'ichi Oishi, Michael Plum, Siegfried M. Rump (eds.)	Algebraic and Numerical Algorithms and Computer-assisted Proofs, 25.-30. September 2005	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2006	DBLP BibTeX RDF
25	Thierry Coquand, Henri Lombardi, Marie-Françoise Roy (eds.)	Mathematics, Algorithms, Proofs, 9.-14. January 2005	Mathematics, Algorithms, Proofs	2006	DBLP BibTeX RDF
25	Borbála Fazekas, Michael Plum, Christian Wieners	Enclosure for the Biharmonic Equation.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Wolfram Luther, Gerhard Haßlinger, Ekaterina Auer, Eva Dyllong, Daniela Traczinski, Holger Traczinski	Integration of reliable algorithms into modeling software.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Philippe Langlois, Stef Graillat, Nicolas Louvet	Compensated Horner Scheme.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Götz Alefeld, Zhengyu Wang	Verification of Solutions for Almost Linear Complementarity Problems.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	James Demmel, Ioana Dumitriu, Olga Holtz	Toward accurate polynomial evaluation in rounded arithmetic (short report).	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Christian Jansson	Rigorous Results in Combinatorial Optimization.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Christian Keil	Lurupa - Rigorous Error Bounds in Linear Programming.	Algebraic and Numerical Algorithms and Computer-assisted Proofs	2005	DBLP BibTeX RDF
25	Harold M. Edwards	Abel and the Concept of the Genus of a Curve.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Virgile Prevosto	Certified mathematical hierarchies: the FoCal system.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Assia Mahboubi	Programming and certifying a CAD algorithm in the Coq system.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Carsten Schneider	Some Notes On "When is 0.999... equal to 1?".	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Paulo Oliva	Unifying Functional Interpretations.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Ihsen Yengui	A dynamical solution of Kronecker's problem.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	César Domínguez 0001, Dominique Duval, Laureano Lambán, Julio Rubio Garcia	Towards Diagrammatic Specifications of Symbolic Computation Systems.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Hervé Perdry, Mariemi Alonso, Henri Lombardi	Henselian Local Rings: Around a Work in Progress.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Harold M. Edwards	Introduction to My Book "Essays in Constructive Mathematics".	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Erik Palmgren	Coequalisers of formal topology.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Philipp Gerhardy, Ulrich Kohlenbach	Generalized metatheorems on the extractability of uniform bounds in functional analysis.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Thierry Coquand, Henri Lombardi, Peter Schuster 0001	A Nilregular Element Property.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Fred Richman	Enabling conditions for interpolated rings.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Tobias Nipkow, Gertrud Bauer	Towards a Verified Enumeration of All Tame Plane Graphs.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Dominique Duval, Jean-Claude Reynaud	Diagrammatic logic and exceptions: an introduction.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Thomas C. Hales	Introduction to the Flyspeck Project.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Marie-Françoise Roy	Subdiscriminant of symmetric matrices are sums of squares.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Ulrich Kohlenbach, Laurentiu Leustean	Approximate fixed points of nonexpansive functions in product spaces.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
25	Bas Spitters	Constructive algebraic integration theory without choice.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
24	Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub	From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.	IFIP TCS	2008	DBLP DOI BibTeX RDF
24	Clemens Grabmayer	Using Proofs by Coinduction to Find "Traditional" Proofs.	CALCO	2005	DBLP DOI BibTeX RDF
24	Rachna Dhamija, J. D. Tygar	Phish and HIPs: Human Interactive Proofs to Detect Phishing Attacks.	HIP	2005	DBLP DOI BibTeX RDF
24	Tobias Nipkow	Structured Proofs in Isar/HOL.	TYPES	2002	DBLP DOI BibTeX RDF
24	Marvin R. G. Schiller, Christoph Benzmüller	Presenting Proofs with Adapted Granularity.	KI	2009	DBLP DOI BibTeX RDF	Adaptive proof presentation, proof tutoring, machine learning, granularity, automated reasoning
24	Yehuda Lindell, Hila Zarosim	Adaptive Zero-Knowledge Proofs and Adaptively Secure Oblivious Transfer.	TCC	2009	DBLP DOI BibTeX RDF
24	Masahiko Sato 0001	A framework for checking proofs naturally.	J. Intell. Inf. Syst.	2008	DBLP DOI BibTeX RDF	Natural framework, Computation and logic, NF/CAL system
24	Vikraman Arvind, Bireswar Das	SZK Proofs for Black-Box Group Problems.	Theory Comput. Syst.	2008	DBLP DOI BibTeX RDF
24	Kosta Dosen, Zoran Petric	Equality of proofs for linear equality.	Arch. Math. Log.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 03F07, 03F52, 03G30, 18C05, 18A40, 18D10, 03F05
24	Paul Valiant	Incrementally Verifiable Computation or Proofs of Knowledge Imply Time/Space Efficiency.	TCC	2008	DBLP DOI BibTeX RDF
24	Chris Peikert, Vinod Vaikuntanathan	Noninteractive Statistical Zero-Knowledge Proofs for Lattice Problems.	CRYPTO	2008	DBLP DOI BibTeX RDF
24	Marek Klonowski, Tomasz Struminski	Proofs of Communication and Its Application for Fighting Spam.	SOFSEM	2008	DBLP DOI BibTeX RDF
24	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
24	David Nowak	A Framework for Game-Based Security Proofs.	ICICS	2007	DBLP DOI BibTeX RDF	security, game, formal verification, proof assistant
24	Lisa Allali	Algorithmic Equality in Heyting Arithmetic Modulo.	TYPES	2007	DBLP DOI BibTeX RDF
24	Michal Armoni	On the role of proofs in a course on design and analysis of algorithms.	ACM SIGCSE Bull.	2006	DBLP DOI BibTeX RDF	algorithms, correctness, proof
24	André Adelsbach, Markus Rohe, Ahmad-Reza Sadeghi	Efficient Implementation of Zero-Knowledge Proofs for Watermark Detection in Multimedia Data.	Trans. Data Hiding Multim. Secur.	2006	DBLP DOI BibTeX RDF