default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID8. ITP 2017: Brasília, Brazil
- Mauricio Ayala-Rincón, César A. Muñoz:
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings. Lecture Notes in Computer Science 10499, Springer 2017, ISBN 978-3-319-66106-3 - Moa Johansson:
Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. 1-11 - Cezary Kaliszyk
, Josef Urban, Jirí Vyskocil:
Automating Formalization by Statistical and Semantic Parsing of Mathematics. 12-27 - Xavier Allamigeon, Ricardo D. Katz:
A Formalization of Convex Polyhedra Based on the Simplex Method. 28-45 - Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. 46-64 - Sophie Bernard:
Formalization of the Lindemann-Weierstrass Theorem. 65-80 - Frédéric Besson, Sandrine Blazy, Pierre Wilke:
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. 81-97 - Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu:
Formal Verification of a Floating-Point Expansion Renormalization Algorithm. 98-113 - David Butler, David Aspinall, Adrià Gascón:
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. 114-130 - Raphaël Cauderlier, Catherine Dubois:
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. 131-147 - Cyril Cohen, Damien Rouhling:
A Formal Proof in Coq of LaSalle's Invariance Principle. 148-163 - Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp:
How to Get More Out of Your Oracles. 164-170 - Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava:
Certifying Standard and Stratified Datalog Inference Engines in SSReflect. 171-188 - Yannick Forster, Gert Smolka:
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. 189-206 - Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer:
Bellerophon: Tactical Theorem Proving for Hybrid Systems. 207-224 - Andrea Gabrielli, Marco Maggesi:
Formalizing Basic Quaternionic Analysis. 225-240 - Lorenzo Gheri, Andrei Popescu:
A Formalized General Theory of Syntax with Bindings. 241-261 - Frédéric Gilbert:
Proof Certificates in PVS. 262-268 - Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler:
Efficient, Verified Checking of Propositional Proofs. 269-284 - Zhe Hou, David Sanán, Alwen Tiu, Yang Liu:
Proof Tactics for Assertions in Separation Logic. 285-303 - Dominik Kirst, Gert Smolka:
Categoricity Results for Second-Order ZF in Dependent Type Theory. 304-318 - Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe:
Making PVS Accessible to Generic Services by Interpretation in a Universal Format. 319-335 - Yanni Kouskoulas, Daniel Genin, Aurora C. Schmidt, Jean-Baptiste Jeannin:
Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. 336-353 - Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. 354-370 - Dominique Larchey-Wendling:
Typing Total Recursive Functions in Coq. 371-388 - Andreas Lochbihler:
Effect Polymorphism in Higher-Order Logic (Proof Pearl). 389-409 - Dirk Pattinson, Mukesh Tiwari:
Schulze Voting as Evidence Carrying Computation. 410-426 - Julian Rosemann, Sigurd Schneider, Sebastian Hack:
Verified Spilling and Translation Validation with Repair. 427-443 - Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola:
A Verified Generational Garbage Collector for CakeML. 444-461 - Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse:
A Formalisation of Consistent Consequence for Boolean Equation Systems. 462-478 - Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz:
Homotopy Type Theory in Lean. 479-495 - Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek:
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. 496-513 - Bohua Zhan:
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. 514-530
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-04 00:39 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
