| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow |
A Formal Proof of the Expressiveness of Deep Learning.  |
ITP  |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Mauricio Ayala-Rincón, César A. Muñoz (eds.) |
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse |
A Formalisation of Consistent Consequence for Boolean Equation Systems. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Lorenzo Gheri, Andrei Popescu 0001 |
A Formalized General Theory of Syntax with Bindings. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhe Hou, David Sanán, Alwen Tiu, Yang Liu 0003 |
Proof Tactics for Assertions in Separation Logic. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Yanni Kouskoulas, Daniel Genin, Aurora C. Schmidt, Jean-Baptiste Jeannin |
Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer |
Bellerophon: Tactical Theorem Proving for Hybrid Systems. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu |
Formal Verification of a Floating-Point Expansion Renormalization Algorithm. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Gilbert 0002 |
Proof Certificates in PVS. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Besson, Sandrine Blazy, Pierre Wilke |
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase, Dennis Müller 0001, Sam Owre, Florian Rabe 0001 |
Making PVS Accessible to Generic Services by Interpretation in a Universal Format. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Dirk Pattinson, Mukesh Tiwari |
Schulze Voting as Evidence Carrying Computation. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp |
How to Get More Out of Your Oracles. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | David Butler 0002, David Aspinall 0001, Adrià Gascón |
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Gabrielli, Marco Maggesi |
Formalizing Basic Quaternionic Analysis. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Moa Johansson |
Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz |
Homotopy Type Theory in Lean. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Bohua Zhan |
AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Anders Schlichtkrull |
Formalization of the Resolution Calculus for First-Order Logic. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth Roe, Scott F. Smith 0001 |
CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond). |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal, Gert Smolka |
Two-Way Automata in Coq. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hölzl |
Formalising Semantics for Expected Running Time of Probabilistic Programs. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Paul Brunet, Damien Pous, Insa Stucke |
Cardinalities of Finite Relations in Coq. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | René Thiemann, Akihisa Yamada 0002 |
Algebraic Numbers in Isabelle/HOL. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah |
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Wimmer 0001 |
Formalized Timed Automata. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Ondrej Kuncar, Andrei Popescu 0001 |
From Types to Sets by Local Type Definitions in Higher-Order Logic. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Joachim Breitner |
Visual Theorem Proving with the Incredible Proof Machine. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann |
Mechanical Verification of a Constructive Proof for FLP. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Nagele, Aart Middeldorp |
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Automatic Functional Correctness Proofs for Functional Search Trees. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Grégoire, Adam Chlipala |
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Abdulaziz, Lawrence C. Paulson |
An Isabelle/HOL Formalisation of Green's Theorem. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Adams |
HOL Zero's Solutions for Pollack-Inconsistency. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich, S. Reza Sefidgar |
Formalizing the Edmonds-Karp Algorithm. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov |
Verified Operational Transformation for Trees. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Fahad Ausaf, Roy Dyckhoff, Christian Urban |
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | David Aspinall 0001, Cezary Kaliszyk |
What's in a Theorem Name? |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
Formally Verified Approximations of Definite Integrals. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Paolo Torrini |
Modular Dependent Induction in Coq, Mendler-Style. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein |
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Romain Aïssat, Frédéric Voisin, Burkhart Wolff |
Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu 0001, Franco Raimondi |
CoSMed: A Confidentiality-Verified Social Media Platform. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Hing-Lun Chan, Michael Norrish |
Proof Pearl: Bounding Least Common Multiples with Triangles. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler, Christoph Traut |
The Flow of ODEs. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Gert Smolka, Kathrin Stark |
Hereditarily Finite Sets in Constructive Type Theory. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Adnan Rashid, Osman Hasan |
On the Formalization of Fourier Transform in Higher-order Logic. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Stephan Merz (eds.) |
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Wenda Li, Lawrence C. Paulson |
A Formal Proof of Cauchy's Residue Theorem. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler, Joshua Schneider 0001 |
Equational Reasoning with Applicative Functors. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven Schäfer, Tobias Tebbi, Gert Smolka |
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Hing-Lun Chan, Michael Norrish |
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | T. V. H. Prathamesh |
Formalising Knot Theory in Isabelle/HOL. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler, Alexandra Maximova |
Stream Fusion for Isabelle's Code Generator - Rough Diamond. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ondrej Kuncar, Andrei Popescu 0001 |
A Consistent Foundation for Isabelle/HOL. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Sternagel, René Thiemann |
Deriving Comparators and Show Functions in Isabelle/HOL. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Gert Smolka, Steven Schäfer, Christian Doczkal |
Transfinite Constructions in Classical Type Theory. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Delphine Demange, David Pichardie |
Validating Dominator Trees for a Fast, Verified Dominance Test. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Régis Spadotti |
A Mechanized Theory of Regular Trees in Dependent Type Theory. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Refinement to Imperative/HOL. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Amortized Complexity Verified. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Besson, Sandrine Blazy, Pierre Wilke |
A Concrete Memory Model for CompCert. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Filip Sieczkowski, Ales Bizjak, Lars Birkedal |
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Arthur Charguéraud, François Pottier |
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Abhishek Anand, Ross A. Knepper |
ROSCoq: Robots Powered by Constructive Reals. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Petar Maksimovic, Alan Schmitt |
HOCore in Coq. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Sigurd Schneider, Gert Smolka, Sebastian Hack |
A Linear First-Order Functional Intermediate Language for Verified Compilers. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Peter Schneider-Kamp |
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Mariano M. Moscato, César A. Muñoz, Andrew P. Smith 0001 |
Affine Arithmetic and Applications to Real-Number Proving. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony C. J. Fox |
Improved Tool Support for Machine-Code Decompilation in HOL4. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Barras, Carst Tankink, Enrico Tassi |
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler |
A Verified Enclosure for the Lorenz Attractor (Rough Diamond). |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Xingyuan Zhang (eds.) |
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
Learning to Parse on Aligned Corpora (Rough Diamond). |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Tuerk, Magnus O. Myreen, Ramana Kumar |
Pattern Matches in HOL: - A New Representation and Improved Code Generation. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Jacques Garrigue |
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce |
Foundational Property-Based Testing. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Benja Fallenstein, Ramana Kumar |
Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Boulmé, Alexandre Maréchal |
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel |
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler, Johannes Hölzl |
Recursive Functions on Lazy Lists via Domains and Topologies. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthieu Sozeau, Nicolas Tabareau |
Universe Polymorphism in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Evmorfia-Iro Bartzia, Pierre-Yves Strub |
A Formal Library for Elliptic Curves in the Coq Proof Assistant. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi |
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
Mechanical Certification of Loop Pipelining Transformations: A Preview. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
Rough Diamond: An Extension of Equivalence-Based Rewriting. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Gross, Adam Chlipala, David I. Spivak |
Experience Implementing a Performant Category-Theory Library in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Chapman, Florian Schanda |
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar |
Formal Verification of Optical Quantum Flip Gate. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Andrei Popescu 0001, Dmitriy Traytel |
Cardinals in Isabelle/HOL. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Kento Emoto, Frédéric Loulergue, Julien Tesson |
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | J Strother Moore |
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Robert Y. Lewis, Cody Roux |
A Heuristic Prover for Real Inequalities. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Dockins |
Formalized, Effective Domain Theory in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu 0001, Dmitriy Traytel |
Truly Modular (Co)datatypes for Isabelle/HOL. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Cock |
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license