default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 62
Volume 62, Number 1, January 2019
- Pierre Boutry, Charly Gries, Julien Narboux
, Pascal Schreck:
Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq. 1-68 - Wenda Li, Grant Olney Passmore, Lawrence C. Paulson:
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. 69-91 - Stijn de Gouw, Frank S. de Boer, Richard Bubel, Reiner Hähnle, Jurriaan Rot, Dominic Steinhöfel:
Verifying OpenJDK's Sort Method for Generic Collections. 93-126 - Mauro Ferrari, Camillo Fiorentini:
Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic. 127-167
Volume 62, Number 2, February 2019
- Jasmin Christian Blanchette, Stephan Merz:
Selected Extended Papers of ITP 2016: Preface. 169-170 - Hing-Lun Chan, Michael Norrish:
Proof Pearl: Bounding Least Common Multiples with Triangles. 171-192 - Thomas Grégoire, Adam Chlipala:
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. 193-213 - Fabian Immler, Christoph Traut:
The Flow of ODEs: Formalization of Variational Equation and Poincaré Map. 215-236 - Ondrej Kuncar, Andrei Popescu:
From Types to Sets by Local Type Definition in Higher-Order Logic. 237-260 - Peter Lammich, S. Reza Sefidgar:
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. 261-280 - Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote:
Formally Verified Approximations of Definite Integrals. 281-300
Volume 62, Number 3, March 2019
- Filip Maric:
Fast Formal Proof of the Erdős-Szekeres Conjecture for Convex Polygons with at Most 6 Points. 301-329 - Arthur Charguéraud, François Pottier:
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. 331-365 - Tobias Nipkow, Hauke Brinkop:
Amortized Complexity Verified. 367-391 - Alexander Leitsch, Anela Lolic:
Extraction of Expansion Trees. 393-430
Volume 62, Number 4, April 2019
- Xingyuan Zhang, Christian Urban:
Selected Extended Papers of ITP 2015: Preface. 431-432 - Frédéric Besson, Sandrine Blazy, Pierre Wilke:
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. 433-480 - Peter Lammich:
Refinement to Imperative HOL. 481-503 - Sylvain Boulmé, Alexandre Maréchal:
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. 505-530 - Ondrej Kuncar, Andrei Popescu:
A Consistent Foundation for Isabelle/HOL. 531-555
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 2024-12-26 00:56 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:
