Search results for "proof-assistants"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
63	Kenneth L. McMillan	Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract).	FMCAD	1998	DBLP DOI BibTeX RDF
51	Adam Chlipala	A verified compiler for an impure functional language.	POPL	2010	DBLP DOI BibTeX RDF	compiler verification, interactive proof assistants
48	Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin	JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants.	IJCAR	2001	DBLP DOI BibTeX RDF
48	Christian Urban, Stefan Berghofer	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF	Lambda-calculus, proof assistants, nominal logic, primitive recursion
45	Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain	Certification of Automated Termination Proofs.	FroCoS	2007	DBLP DOI BibTeX RDF
45	Adam Chlipala	Parametric higher-order abstract syntax for mechanized semantics.	ICFP	2008	DBLP DOI BibTeX RDF	type-theoretic semantics, dependent types, compiler verification, interactive proof assistants
39	David Aspinall 0001	Proof General: A Generic Tool for Proof Development.	TACAS	2000	DBLP DOI BibTeX RDF
39	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
38	Benjamin C. Pierce	Lambda, the ultimate TA: using a proof assistant to teach programming language foundations.	ICFP	2009	DBLP DOI BibTeX RDF	programming languages, pedagogy, proof assistants
36	Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier 0002, Claus-Peter Wirth	A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity.	MKM	2005	DBLP DOI BibTeX RDF
36	Jesús Aransay, César Domínguez 0001	Modelling Differential Structures in Proof Assistants: The Graded Case.	EUROCAST	2009	DBLP DOI BibTeX RDF
34	Hans-Jörg Schurr	Stronger SMT Solvers for Proof Assistants: Proofs, Quantifier Simplification, Strategy Schedules. (Consolidation des solveurs SMT pour les assistants de preuve: preuves, simplification des quantificateurs, planification de stratégies).		2022	RDF
34	Benjamin C. Pierce	Proof Assistants as Teaching Assistants: A View from the Trenches.	ITP	2010	DBLP DOI BibTeX RDF
33	Carsten Schürmann 0001, Jeffrey Sarnat	Structural Logical Relations.	LICS	2008	DBLP DOI BibTeX RDF	Twelf, Normalization, Logical Frameworks, Cut-Elimination, Logical Relations
33	Andreas Abel 0001, Thierry Coquand, Peter Dybjer	On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.	FLOPS	2008	DBLP DOI BibTeX RDF
33	Claudio Sacerdoti Coen	From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.	MKM	2003	DBLP DOI BibTeX RDF
33	Olivier Pons	Generalization in Type Theory Based Proof Assistants.	TYPES	2000	DBLP DOI BibTeX RDF
30	Cristian S. Calude, Christine Müller	Formal Proof: Reconciling Correctness and Understanding.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
30	Eric Deplagne, Claude Kirchner	Deduction versus Computation: The Case of Induction.	AISC	2002	DBLP DOI BibTeX RDF
27	Lawrence C. Paulson, Kong Woei Susanto	Source-Level Proof Reconstruction for Interactive Theorem Proving.	TPHOLs	2007	DBLP DOI BibTeX RDF
27	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
26	Max Schäfer, Torbjörn Ekman 0001, Oege de Moor	Challenge proposal: verification of refactorings.	PLPV	2009	DBLP DOI BibTeX RDF	refactoring, proof assistants, mechanical verification
26	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
26	Nick Benton, Chung-Kil Hur	Biorthogonality, step-indexing and compiler correctness.	ICFP	2009	DBLP DOI BibTeX RDF	biorthogonality, step-indexing, denotational semantics, proof assistants, compiler verification
26	Nick Benton, Nicolas Tabareau	Compiling functional types to relational specifications for low level imperative code.	TLDI	2009	DBLP DOI BibTeX RDF	separation logic, proof assistants, compiler verification, relational parametricity, type soundness
26	Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Marc Wagner 0001	Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	Mathematical knowledge management, system architecture, proof assistants
26	Antonio Maña, Gimena Pujol	Towards Formal Specification of Abstract Security Properties.	ARES	2008	DBLP DOI BibTeX RDF	Formal Models, Security Properties, Proof assistants
26	Bart Jacobs 0001, Sjaak Smetsers, Ronny Wichers Schreur	Code-carrying theories.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Compression, Code generation, Functional languages, Unification, PVS, Proof assistants
26	Adam Chlipala	A certified type-preserving compiler from lambda calculus to assembly language.	PLDI	2007	DBLP DOI BibTeX RDF	denotational semantics, dependent types, compiler verification, interactive proof assistants
26	Nick Benton, Uri Zarfaty	Formalizing and verifying semantic type soundness of a simple compiler.	PPDP	2007	DBLP DOI BibTeX RDF	relational para-metricity, separation logic, proof assistants, compiler verification, type soundness
26	Adam Chlipala	Modular development of certified program verifiers with a proof assistant.	ICFP	2006	DBLP DOI BibTeX RDF	programming with dependent types, proof-carrying code, interactive proof assistants
26	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Verifying Haskell Programs by Combining Testing and Proving.	QSIC	2003	DBLP DOI BibTeX RDF	BDDs and Haskell, program verification, random testing, type theory, proof-assistants
26	Steven Shapiro, Yves Lespérance, Hector J. Levesque	The cognitive agents specification language and verification environment for multiagent systems.	AAMAS	2002	DBLP DOI BibTeX RDF	agent specification languages, theorem proving, proof assistants, verification tools
24	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
24	J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro	Verification of Program Properties Using Different Theorem Provers: A Case Study.	EUROCAST	2007	DBLP DOI BibTeX RDF
21	Rajeev Goré	Machine Checking Proof Theory: An Application of Logic to Logic.	ICLA	2009	DBLP DOI BibTeX RDF
21	Guillaume Melquiond	Proving Bounds on Real-Valued Functions with Computations.	IJCAR	2008	DBLP DOI BibTeX RDF
21	William Billingsley, Peter Robinson 0001	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
21	Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub	Building Decision Procedures in the Calculus of Inductive Constructions.	CSL	2007	DBLP DOI BibTeX RDF	Calculus of Inductive Constructions, Decision procedures, Theorem provers
21	Olivier Boite	Proof Reuse with Extended Inductive Types.	TPHOLs	2004	DBLP DOI BibTeX RDF
21	Claudio Sacerdoti Coen	Mathematical Libraries as Proof Assistant Environments.	MKM	2004	DBLP DOI BibTeX RDF
21	Robin Milner	Graphical Theories of Interactive Systems: Can a Proof Assistant Help?	TPHOLs	2000	DBLP DOI BibTeX RDF
21	Mario Gleirscher, Robert Sachtleben, Jan Peleska 0001	Qualification of Proof Assistants, Checkers, and Generators: Where Are We and What Next?	CoRR	2023	DBLP DOI BibTeX RDF
21	Mario Gleirscher, Robert Sachtleben, Jan Peleska 0001	Qualification of proof assistants, checkers, and generators: Where are we and what next?	Sci. Comput. Program.	2023	DBLP DOI BibTeX RDF
21	Colin S. Gordon, Sergey Matskevich	Natural Language Specifications in Proof Assistants.	CoRR	2022	DBLP DOI BibTeX RDF
21	Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.	CoRR	2022	DBLP BibTeX RDF
21	Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.	ITP	2022	DBLP DOI BibTeX RDF
21	Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter	The Multiverse: Logical Modularity for Proof Assistants.	CoRR	2021	DBLP BibTeX RDF
21	João R. M. Nicola, Giancarlo Guizzardi	On the Role of Automated Proof-Assistants in the Formalization of Upper Ontologies.	JOWO	2021	DBLP BibTeX RDF
21	Cristian S. Calude	Gödel Incompleteness and Proof-Assistants Extended Abstract.	SYNASC	2021	DBLP DOI BibTeX RDF
21	Mohamed Yacine El Haddad	Integrating Automated Theorem Provers in Proof Assistants. (Utiliser des démonstrateurs automatiques dans un assistant à la preuve).		2021	RDF
21	Fritjof Bornebusch	Coq meets CλaSH: proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages		2021	RDF
21	Guangshuai Mo, Yan Xiong, Wenchao Huang, Lu Ma	Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies.	BigCom	2020	DBLP DOI BibTeX RDF
21	Adam Chlipala	Proof assistants at the hardware-software interface (invited talk).	CPP	2020	DBLP DOI BibTeX RDF
21	Kaiyu Yang, Jia Deng 0001	Learning to Prove Theorems via Interacting with Proof Assistants.	CoRR	2019	DBLP BibTeX RDF
21	Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun	Design of Point-and-Click User Interfaces for Proof Assistants.	ICFEM	2019	DBLP DOI BibTeX RDF
21	Kaiyu Yang, Jia Deng 0001	Learning to Prove Theorems via Interacting with Proof Assistants.	ICML	2019	DBLP BibTeX RDF
21	François Thiré	Sharing a Library between Proof Assistants: Reaching out to the HOL Family.	LFMTP@FSCD	2018	DBLP DOI BibTeX RDF
21	Insa Stucke	Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants.	RAMiCS	2017	DBLP DOI BibTeX RDF
21	Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu 0001, Dmitriy Traytel	Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.	ESOP	2017	DBLP DOI BibTeX RDF
21	Sylvie Boldo, Catherine Lelay, Guillaume Melquiond	Formalization of real analysis: a survey of proof assistants and libraries.	Math. Struct. Comput. Sci.	2016	DBLP DOI BibTeX RDF
21	Li-An Yang, Jui-Pin Liu, Chao-Hong Chen, Ying-Ping Chen	Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants.	CoRR	2016	DBLP BibTeX RDF
21	Li-An Yang, Jui-Pin Liu, Chao-Hong Chen, Ying-Ping Chen	Automatically proving mathematical theorems with evolutionary algorithms and proof assistants.	CEC	2016	DBLP DOI BibTeX RDF
21	Stergios Chatzikyriakidis, Zhaohui Luo	Proof Assistants for Natural Language Semantics.	LACL	2016	DBLP DOI BibTeX RDF
21	Abhishek Anand	Trust in Proof Assistants: Opportunities and Limitations.		2016	RDF
21	Adam Grabowski, Artur Kornilowicz, Christoph Schwarzweller	Equality in computer proof-assistants.	FedCSIS	2015	DBLP DOI BibTeX RDF
21	Anders Schlichtkrull	Formalization of Algorithms and Logical Inference Systems in Proof Assistants.	SCAI	2015	DBLP DOI BibTeX RDF
21	Ondrej Kuncar	Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.	CPP	2015	DBLP DOI BibTeX RDF
21	Robert L. Constable	Proof Assistants and the Dynamic Nature of Formal Theories.	PxTP	2012	DBLP BibTeX RDF
21	Robert L. Constable	Proof Assistants and the Dynamic Nature of Formal Theories.	ATx/WInG@IJCAR	2012	DBLP DOI BibTeX RDF
21	Gabriel Dos Reis, David C. J. Matthews, Yue Li	Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
21	Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, Stephan Schulz 0001 (eds.)	Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008	LPAR Workshops	2008	DBLP BibTeX RDF
21	Florian Rabe 0001, Michael Kohlhase	An Exchange Format for Modular Knowledge.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Stefan Hetzl, Alexander Leitsch, Daniel Weller 0001, Bruno Woltzenlogel Paleo	Transforming and Analyzing Proofs in the CERES-System.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz	A TLA+ Proof System.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Josef Urban	Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Loic Pottier	Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics.	LPAR Workshops	2008	DBLP BibTeX RDF
21	José Faustino Fragoso Femenin dos Santos, Vasco M. Manquinho	Learning Techniques for Pseudo-Boolean Solving.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Michael Balser, Simon Bäumler, Wolfgang Reif, Gerhard Schellhorn	Interactive Verification of Concurrent Systems using Symbolic Execution.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Proofs and Refutations, and Z3.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Geoff Sutcliffe	The SZS Ontologies for Automated Reasoning Software.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue	Complete Pruning Methods and a Practical Search Strategy for SOL.	LPAR Workshops	2008	DBLP BibTeX RDF
21	Martin Strecker	Modeling and Verifying Graph Transformations in Proof Assistants.	TERMGRAPH@ETAPS	2007	DBLP DOI BibTeX RDF
21	Maarten de Mol, Marko C. J. D. van Eekelen, Rinus Plasmeijer	A Single-Step Term-Graph Reduction System for Proof Assistants.	AGTIVE	2007	DBLP DOI BibTeX RDF
21	Adam Chlipala	Position Paper: Thoughts on Programming with Proof Assistants.	PLPV@IJCAR	2006	DBLP DOI BibTeX RDF
21	Cezary Kaliszyk	Web Interfaces for Proof Assistants.	UITP@FLoC	2006	DBLP DOI BibTeX RDF
21	Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker	Towards formalising AADL in Proof Assistants.	FESCA@ETAPS	2005	DBLP DOI BibTeX RDF
21	Norbert Völker	Thoughts on Requirements and Design Issues of User Interfaces for Proof Assistants.	UITP@TPHOLs	2003	DBLP DOI BibTeX RDF
21	Quang Huy Nguyen 0002, Claude Kirchner, Hélène Kirchner	External Rewriting for Skeptical Proof Assistants.	J. Autom. Reason.	2002	DBLP DOI BibTeX RDF
21	Henk Barendregt, Arjeh M. Cohen	Electronic Communication of Mathematics and the Interaction of Computer Algebra Systems and Proof Assistants.	J. Symb. Comput.	2001	DBLP DOI BibTeX RDF
21	Henk Barendregt, Herman Geuvers	Proof-Assistants Using Dependent Type Systems.	Handbook of Automated Reasoning	2001	DBLP DOI BibTeX RDF
21	Rix Groenboom, Chris Hendriks, Indra Polak, Jan Terlouw, Jan Tijmen Udding	Algebraic Proof Assistants in HOL.	MPC	1995	DBLP DOI BibTeX RDF
18	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
18	Paul Brauner, Clément Houtmann, Claude Kirchner	Principles of Superdeduction.	LICS	2007	DBLP DOI BibTeX RDF
18	Nicolas Oury	Pattern matching coverage checking with dependent types using set approximations.	PLPV	2007	DBLP DOI BibTeX RDF	coverage checking, set approximation, pattern matching
18	Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann	An Integration of HOL and ACL2.	FMCAD	2006	DBLP DOI BibTeX RDF
18	Marko Luther	More On Implicit Syntax.	IJCAR	2001	DBLP DOI BibTeX RDF
18	Furio Honsell, Marino Miculan	A Natural Deduction Approach to Dynamic Logic.	TYPES	1995	DBLP DOI BibTeX RDF
15	Rafael del Vado Vírseda	A higher-order logical framework for the algorithmic debugging and verification of declarative programs.	PPDP	2009	DBLP DOI BibTeX RDF	algorithmic debugging, declarative verification, multiparadigm declarative programming, lambda calculus
15	Pierre Courtieu, Julien Forest, Xavier Urbain	Certifying a Termination Criterion Based on Graphs, without Graphs.	TPHOLs	2008	DBLP DOI BibTeX RDF