Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 63
Volume 63, Number 1, June 2019
- Gilles Barthe, Gustavo Betarte
, Juan Diego Campo, Carlos Luna:
System-Level Non-interference of Constant-Time Cryptography. Part I: Model. 1-51 - Peter Lammich, Andreas Lochbihler:
Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. 53-94 - Gabriel Ebner, Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller:
On the Generation of Quantified Lemmas. 95-126 - Tomás Peitl, Friedrich Slivovsky, Stefan Szeider:
Long-Distance Q-Resolution with Dependency Schemes. 127-155
Volume 63, Number 2, August 2019
- Peter LeFanu Lumsdaine, Nicolas Tabareau:
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. 157-158 - Marc Bezem, Thierry Coquand, Simon Huber:
The Univalence Axiom in Cubical Sets. 159-171 - Simon Huber:
Canonicity for Cubical Type Theory. 173-210 - Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi:
Guarded Cubical Type Theory. 211-253 - Guillaume Brunerie:
The James Construction and π4(S3) in Homotopy Type Theory. 255-284 - Benedikt Ahrens, Ralph Matthes, Anders Mörtberg:
From Signatures to Monads in UniMath. 285-318 - Mauricio Ayala-Rincón, César A. Muñoz:
Selected Extended Papers of ITP 2017 - Preface. 319-321 - Xavier Allamigeon, Ricardo D. Katz:
A Formalization of Convex Polyhedra Based on the Simplex Method. 323-345 - Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. 347-368 - Frédéric Besson, Sandrine Blazy, Pierre Wilke:
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. 369-392 - Yannick Forster, Gert Smolka:
Call-by-Value Lambda Calculus as a Model of Computation in Coq. 393-413 - Dominik Kirst, Gert Smolka:
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. 415-438 - Andreas Lochbihler:
Effect Polymorphism in Higher-Order Logic (Proof Pearl). 439-462 - Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola:
A Verified Generational Garbage Collector for CakeML. 463-488 - Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek:
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. 489-515 - Bohua Zhan:
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. 517-538
Volume 63, Number 3, October 2019
- Jia Tao:
A PSpace Algorithm for Acyclic Epistemic DL ALCS5m. 539-555 - Cezary Kaliszyk, Karol Pak:
Semantics of Mizar as an Isabelle Object Logic. 557-595 - Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda:
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. 597-623 - Dale Miller:
Mechanized Metatheory Revisited. 625-665 - Hing-Lun Chan, Michael Norrish:
Classification of Finite Fields with Applications. 667-693 - Luís Cruz-Filipe, João Marques-Silva, Peter Schneider-Kamp:
Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. 695-722 - Wenxi Wang, Harald Søndergaard, Peter J. Stuckey:
Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation. 723-762 - Mohammad Abdulaziz, Lawrence C. Paulson:
An Isabelle/HOL Formalisation of Green's Theorem. 763-786 - Li-Ming Li, Zhi-Ping Shi, Yong Guan, Qianying Zhang, Yong-Dong Li:
Formalization of Geometric Algebra in HOL Light. 787-808
Volume 63, Number 4, December 2019
Special Issue: Selected Extended Papers of NFM 2017
- Iliano Cervesato, Maribel Fernández:
Preface to the Special Issue on Linearity. 809-811 - Patrick Baillot, Gilles Barthe, Ugo Dal Lago:
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. 813-855 - Quentin Heath, Dale Miller:
A Proof Theory for Model Checking. 857-885 - Ian Mackie:
Linear Numeral Systems. 887-909 - Matteo Acclavio:
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics. 911-939 - Luca Paolini, Mauro Piccolo, Margherita Zorzi:
QPCF: Higher-Order Languages and Quantum Circuits. 941-966 - Mohamed Yousri Mahmoud, Amy P. Felty:
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. 967-1002 - Clark W. Barrett, Temesghen Kahsai:
Selected Extended Papers of NFM 2017: Preface. 1003-1004 - Andrew Sogokon, Paul B. Jackson, Taylor T. Johnson:
Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants. 1005-1029 - Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia:
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. 1031-1053 - Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto, Michael Francis:
Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae. 1055-1075 - Hadar Frenkel, Orna Grumberg, Sarai Sheinvald:
An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains. 1077-1101 - Bernhard K. Aichernig, Martin Tappler:
Efficient Active Automata Learning via Mutation Testing. 1103-1134
a service of 
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-05-31 18:43 CEST 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:
