Search results for "proofs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
23	Adi Shamir	IP = PSPACE.	J. ACM	1992	DBLP DOI BibTeX RDF	IP, interactive proofs, PSPACE
23	G. A. Venkatesh, Charles N. Fischer	SPARE: A Development Environment For Program Analysis Algorithms.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	program analysis specifications, high-level specification language, SPARE, structured program analysis refinement environment, denotational specification, formal specification, testing, software tools, software tools, programming environments, specification languages, program testing, development environment, correctness proofs
20	Benoît Libert	Vector Commitments with Proofs of Smallness: Short Range Proofs and More.	Public Key Cryptography (2)	2024	DBLP DOI BibTeX RDF
20	Nao Hirokawa, Dohan Kim 0001, Kiraku Shintani, René Thiemann	Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs.	CPP	2024	DBLP DOI BibTeX RDF
20	Amir Farahmand Parsa, Meghdad Ghari	On Boolean Algebraic Structure of Proofs: Towards an Algebraic Semantics for the Logic of Proofs.	Stud Logica	2023	DBLP DOI BibTeX RDF
20	Sara Ayhan	Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.	CoRR	2023	DBLP DOI BibTeX RDF
20	Léo Colisson, Garazi Muguruza, Florian Speelman	Oblivious Transfer from Zero-Knowledge Proofs, or How to Achieve Round-Optimal Quantum Oblivious Transfer and Zero-Knowledge Proofs on Quantum States.	CoRR	2023	DBLP DOI BibTeX RDF
20	Morten Jokumsen, Torben Pryds Pedersen, Martin Schmidt Daugaard, Daniel Tschudi, Mikkel Wienberg Madsen, Thomas Wisbech	Verifiable proofs for the energy supply chain: small proofs brings you a long way.	Energy Inform.	2023	DBLP DOI BibTeX RDF
20	Léo Colisson, Garazi Muguruza, Florian Speelman	Oblivious Transfer from Zero-Knowledge Proofs, or How to Achieve Round-Optimal Quantum Oblivious Transfer and Zero-Knowledge Proofs on Quantum States.	IACR Cryptol. ePrint Arch.	2023	DBLP BibTeX RDF
20	Léo Colisson, Garazi Muguruza, Florian Speelman	Oblivious Transfer from Zero-Knowledge Proofs - Or How to Achieve Round-Optimal Quantum Oblivious Transfer and Zero-Knowledge Proofs on Quantum States.	ASIACRYPT (8)	2023	DBLP DOI BibTeX RDF
20	Kunming Jiang, Devora Chait-Roth, Zachary DeStefano, Michael Walfish, Thomas Wies	Less is more: refinement proofs for probabilistic proofs.	SP	2023	DBLP DOI BibTeX RDF
20	Foteini Baldimtsi, Panagiotis Chatzigiannis, S. Dov Gordon, Phi Hung Le, Daniel McVicker	gOTzilla: Efficient Disjunctive Zero-Knowledge Proofs from MPC in the Head, with Application to Proofs of Assets in Cryptocurrencies.	Proc. Priv. Enhancing Technol.	2022	DBLP DOI BibTeX RDF
20	Kunming Jiang, Devora Chait-Roth, Zachary DeStefano, Michael Walfish, Thomas Wies	Less is more: refinement proofs for probabilistic proofs.	IACR Cryptol. ePrint Arch.	2022	DBLP BibTeX RDF
20	Foteini Baldimtsi, Panagiotis Chatzigiannis, S. Dov Gordon, Phi Hung Le, Daniel McVicker	gOTzilla: Efficient Disjunctive Zero-Knowledge Proofs from MPC in the Head, with Application to Proofs of Assets in Cryptocurrencies.	IACR Cryptol. ePrint Arch.	2022	DBLP BibTeX RDF
20	Simon Weisgerber	Visual Proofs as Counterexamples to the Standard View of Informal Mathematical Proofs?	Diagrams	2022	DBLP DOI BibTeX RDF
20	David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin	Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs.	LICS	2022	DBLP DOI BibTeX RDF
20	Shujun Zhang, Naoki Nishida 0001	On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs.	FLOPS	2022	DBLP DOI BibTeX RDF
20	Catherine Dubois, Nicolas Magaud, Alain Giorgetti	Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families.	TYPES	2022	DBLP DOI BibTeX RDF
20	Benny Applebaum, Eyal Golombek	On the Randomness Complexity of Interactive Proofs and Statistical Zero-Knowledge Proofs.	IACR Cryptol. ePrint Arch.	2021	DBLP BibTeX RDF
20	Benny Applebaum, Eyal Golombek	On the Randomness Complexity of Interactive Proofs and Statistical Zero-Knowledge Proofs.	ITC	2021	DBLP DOI BibTeX RDF
20	Davide Catta	Les preuves vues comme des jeux et réciproquement: sémantique dialogique de langages naturel ou logiques. (Proofs as games and games as proofs: dialogical semantics of logical and natural languages).		2021	RDF
20	Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton	CertRL: formalizing convergence proofs for value and policy iteration in Coq.	CPP	2021	DBLP DOI BibTeX RDF
20	Edward Hermann Haeusler	On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing M⊃ Super-Polynomial Proofs.	CoRR	2020	DBLP BibTeX RDF
20	Johannes Altmanninger, Adrian Rebola-Pardo	Frying the egg, roasting the chicken: unit deletions in DRAT proofs.	CPP	2020	DBLP DOI BibTeX RDF
20	Tal Moran, Ilan Orlov	Simple Proofs of Space-Time and Rational Proofs of Storage.	CRYPTO (1)	2019	DBLP DOI BibTeX RDF
20	Matteo Acclavio, Lutz Straßburger	From Syntactic Proofs to Combinatorial Proofs.	IJCAR	2018	DBLP DOI BibTeX RDF
20	Gabriel Ebner, Matthias Schlaipfer	Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs.	PAAR@FLoC	2018	DBLP BibTeX RDF
20	Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar	Proofs in conflict-driven theory combination.	CPP	2018	DBLP DOI BibTeX RDF
20	Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman	Adapting proof automation to adapt proofs.	CPP	2018	DBLP DOI BibTeX RDF
20	Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada 0002	Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper).	CPP	2018	DBLP DOI BibTeX RDF
20	Brigitte Pientka	POPLMark reloaded: mechanizing logical relations proofs (invited talk).	CPP	2018	DBLP DOI BibTeX RDF
20	Guillaume Allais, James Chapman 0001, Conor McBride, James McKinna	Type-and-scope safe programs and their proofs.	CPP	2017	DBLP DOI BibTeX RDF
20	Reuben N. S. Rowe, James Brotherston	Automatic cyclic termination proofs for recursive procedures in separation logic.	CPP	2017	DBLP DOI BibTeX RDF
20	Tal Moran, Ilan Orlov	Proofs of Space-Time and Rational Proofs of Storage.	IACR Cryptol. ePrint Arch.	2016	DBLP BibTeX RDF
20	Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier	Semi-intelligible Isar Proofs from Machine-Generated Proofs.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
20	Victor W. Marek	All about Proofs, Proofs for All, Bruno Woltzenlogel Paleo and David Delahaye, Eds., College Publications, Series Mathematical Logic and Foundations, vol. 55., 2015. Paperback, ISBN 978-1-84890-166-7, vii + 240 pages.	Theory Pract. Log. Program.	2016	DBLP DOI BibTeX RDF
20	Aggelos Kiayias, Nikolaos Lamprou, Aikaterini-Panagiota Stouka	Proofs of Proofs of Work with Sublinear Complexity.	Financial Cryptography Workshops	2016	DBLP DOI BibTeX RDF
20	Catherine Dubois, Alain Giorgetti, Richard Genestier	Tests and Proofs for Enumerative Combinatorics.	TAP@STAF	2016	DBLP DOI BibTeX RDF
20	Nathan Fulton, André Platzer	A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics.	CPP	2016	DBLP DOI BibTeX RDF
20	Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.	CPP	2016	DBLP DOI BibTeX RDF
20	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CPP	2015	DBLP DOI BibTeX RDF
20	Achim D. Brucker, Jacques Julliand	Editorial for the special issue of STVR on tests and proofs volume 1: tests and proofs in model-based testing.	Softw. Test. Verification Reliab.	2014	DBLP DOI BibTeX RDF
20	Achim D. Brucker, Jacques Julliand	Editorial for the special issue of STVR on tests and proofs volume 2: tests and proofs for improving the generation time and quality of test data suites.	Softw. Test. Verification Reliab.	2014	DBLP DOI BibTeX RDF
20	Göran Sundholm	Demonstrations Versus Proofs, Being an Afterword to Constructions, Proofs, and the Meaning of the Logical Constants.	Judgement and the Epistemic Foundation of Logic	2013	DBLP DOI BibTeX RDF
20	Steffen Juilf Smolka, Jasmin Christian Blanchette	Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs.	PxTP@CADE	2013	DBLP DOI BibTeX RDF
20	Ulrich Berger 0001, Monika Seisenberger, Gregory J. M. Woods	Extracting Imperative Programs from Proofs: In-place Quicksort.	TYPES	2013	DBLP DOI BibTeX RDF
20	Dale Miller 0001, Alwen Tiu	Extracting Proofs from Tabled Proof Search.	CPP	2013	DBLP DOI BibTeX RDF
20	Hing-Lun Chan, Michael Norrish	A String of Pearls: Proofs of Fermat's Little Theorem.	CPP	2012	DBLP DOI BibTeX RDF
20	Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin	Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.	CPP	2012	DBLP DOI BibTeX RDF
20	Geoff Sutcliffe, Cynthia Chang, Deborah L. McGuinness, Timothy Lebo, Li Ding 0001, Paulo Pinheiro da Silva	Combining Proofs to form Different Proofs.	PxTP	2011	DBLP BibTeX RDF
20	Patrice Godefroid	Tests from Proofs.	TAP@TOOLS	2011	DBLP DOI BibTeX RDF
20	Sorin Stratulat, Vincent Demange	Automated Certification of Implicit Induction Proofs.	CPP	2011	DBLP DOI BibTeX RDF
20	Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber	Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.	CPP	2011	DBLP DOI BibTeX RDF
20	Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech	Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience.	CPP	2011	DBLP DOI BibTeX RDF
20	Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie	Modular SMT Proofs for Fast Reflexive Checking Inside Coq.	CPP	2011	DBLP DOI BibTeX RDF
20	Thi Minh Tuyen Nguyen, Claude Marché	Hardware-Dependent Proofs of Numerical Programs.	CPP	2011	DBLP DOI BibTeX RDF
20	Alessandra Carbone	A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs.	Inf. Comput.	2010	DBLP DOI BibTeX RDF
20	Geoff Sutcliffe, Cynthia Chang, Li Ding 0001, Deborah L. McGuinness, Paulo Pinheiro da Silva	Different Proofs are Good Proofs.	EMSQMS@IJCAR	2010	DBLP DOI BibTeX RDF
20	Michael D. Ernst	How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback.	TAP@TOOLS	2010	DBLP DOI BibTeX RDF
20	Ulrich Berger 0001, Monika Seisenberger	Proofs, Programs, Processes.	CiE	2010	DBLP DOI BibTeX RDF
20	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	CoRR	2008	DBLP BibTeX RDF
20	Koen Claessen, Hans Svensson	Finding Counter Examples in Induction Proofs.	TAP	2008	DBLP DOI BibTeX RDF
20	Nathan Segerlind	On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs.	Electron. Colloquium Comput. Complex.	2007	DBLP BibTeX RDF
20	Amitabh Saxena	Additive Proofs of Knowledge - A New Notion for Non-Interactive Proofs.	SECRYPT	2007	DBLP BibTeX RDF
20	Christian Engel 0002, Reiner Hähnle	Generating Unit Tests from Formal Proofs.	TAP	2007	DBLP DOI BibTeX RDF	theorem proving, program verification, model-based testing, unit testing, symbolic execution, test coverage, white-box testing
20	Amitabh Saxena	Additive Proofs of Knowledge - A New Notion For Non-Interactive Proofs.	IACR Cryptol. ePrint Arch.	2005	DBLP BibTeX RDF
20	Hans de Nivelle	Translation of resolution proofs into short first-order proofs without choice axioms.	Inf. Comput.	2005	DBLP DOI BibTeX RDF
20	Prahladh Harsha	Robust Probabilistically Checkable Proofs of proximity and shorter Robust Probabilistically Checkable Proofs.		2004	RDF
20	Laurent Théry	Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs.	UITP@TPHOLs	2003	DBLP DOI BibTeX RDF
20	Hans de Nivelle	Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms.	CADE	2003	DBLP DOI BibTeX RDF
20	Silvia Ghilezan, Pierre Lescanne	Classical Proofs, Typed Processes, and Intersection Types: Extended Abstract.	TYPES	2003	DBLP DOI BibTeX RDF
20	Susumu Hayashi, Ryosuke Sumitomo, Ken-ichiro Shii	Towards the animation of proofs - testing proofs by examples.	Theor. Comput. Sci.	2002	DBLP DOI BibTeX RDF
20	Jesper Buus Nielsen	Separating Random Oracle Proofs from Complexity Theoretic Proofs: The Non-committing Encryption Case.	CRYPTO	2002	DBLP DOI BibTeX RDF
20	Yuri Gurevich	Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand.	Current Trends in Theoretical Computer Science	2001	DBLP BibTeX RDF
20	Giovanni Di Crescenzo, Russell Impagliazzo	Proofs of Membership vs. Proofs of Knowledge.	CCC	1998	DBLP DOI BibTeX RDF
20	Kouichi Sakurai	Practical Proofs of Knowledge without Relying on Theoretical Proofs of Membership on Languages.	Theor. Comput. Sci.	1997	DBLP DOI BibTeX RDF
20	Gilles Dowek	A Type-Free Formalization of Mathematics where Proofs are Objects.	TYPES	1996	DBLP DOI BibTeX RDF
20	Yuri Gurevich	Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand.	Bull. EATCS	1995	DBLP BibTeX RDF
20	Stephan Schmitt, Christoph Kreitz	On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs.	TABLEAUX	1995	DBLP DOI BibTeX RDF
20	Kouichi Sakurai	On Separating Proofs of Knowledge from Proofs of Membership of Languages and Its Application to Secure Identification Schemes (Extended Abstract).	COCOON	1995	DBLP DOI BibTeX RDF
20	Ulrich Berger 0001, Helmut Schwichtenberg	The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs.	TYPES	1995	DBLP DOI BibTeX RDF
20	Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang	Machine proofs in geometry - automated production of readable proofs for geometry theorems.		1994	RDF
20	Martin W. Bunder	Some Consistency Proofs and a Characterization of Inconsistency Proofs in Illative Combinatory Logic.	J. Symb. Log.	1987	DBLP DOI BibTeX RDF
20	Thomas P. Murtagh	Redundant Proofs of Non-Interference in Levin-Gries CSP Program Proofs.	Acta Informatica	1987	DBLP DOI BibTeX RDF
20	Thomas P. Murtagh	Eliminating Proofs of Non-interference from Levin-Gries CSP Program Proofs.	ICDCS	1986	DBLP BibTeX RDF
19	Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, Julien Forest	A3PAT, an approach for certified automated termination proofs.	PEPM	2010	DBLP DOI BibTeX RDF	termination, term rewriting, automated reasoning, formal proof
19	Madhu Sudan 0001	Probabilistically checkable proofs.	Commun. ACM	2009	DBLP DOI BibTeX RDF
19	Georg Fuchsbauer, David Pointcheval	Proofs on Encrypted Values in Bilinear Groups and an Application to Anonymity of Signatures.	Pairing	2009	DBLP DOI BibTeX RDF
19	Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Effective interactive proofs for higher-order imperative programs.	ICFP	2009	DBLP DOI BibTeX RDF	functional programming, dependent types, separation logic, interactive proof assistants
19	Giuseppe Ateniese, Seny Kamara, Jonathan Katz	Proofs of Storage from Homomorphic Identification Protocols.	ASIACRYPT	2009	DBLP DOI BibTeX RDF
19	Lujo Bauer, Limin Jia 0001, Michael K. Reiter, David Swasey	xDomain: cross-border proofs of access.	SACMAT	2009	DBLP DOI BibTeX RDF	logic-based access control, trust management, distributed authorization
19	Jan Camenisch, Aggelos Kiayias, Moti Yung	On the Portability of Generalized Schnorr Proofs.	EUROCRYPT	2009	DBLP DOI BibTeX RDF
19	Malgorzata Biernacka, Dariusz Biernacki	Context-based proofs of termination for typed delimited-control operators.	PPDP	2009	DBLP DOI BibTeX RDF	reducibility predicates, type system, continuation-passing style, delimited continuations, reduction semantics
19	Eduardo Bonelli, Federico Feller	The Logic of Proofs as a Foundation for Certifying Mobile Computation.	LFCS	2009	DBLP DOI BibTeX RDF
19	Chunming Tang 0003, Dingyi Pei, Xiaofeng Wang, Zhuojun Liu	Delegateable signatures based on non-interactive witness indistinguishable and non-interactive witness hiding proofs.	Sci. China Ser. F Inf. Sci.	2008	DBLP DOI BibTeX RDF	delegateable signature, non-interactive witness indistinguishable, non-interactive witness hiding, ?-protocol, non-interactive zero-knowledge
19	Josef Urban, Geoff Sutcliffe	ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	verification, automated reasoning, Formalized mathematics
19	John C. Reynolds	Readable Formal Proofs.	VSTTE	2008	DBLP DOI BibTeX RDF
19	Iman Poernomo	Proofs-as-Model-Transformations.	ICMT@TOOLS	2008	DBLP DOI BibTeX RDF
19	Timothy Y. Chow	Almost-Natural Proofs.	FOCS	2008	DBLP DOI BibTeX RDF
19	Eli Ben-Sasson, Jakob Nordström	Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.	FOCS	2008	DBLP DOI BibTeX RDF