Isabelle/HOL. A proof assistant for higher-order logic

Related Items

Theorem proving graph grammars with attributes and negative application conditions ⋮ Using relation-algebraic means and tool support for investigating and computing bipartitions ⋮ Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A decision procedure for (co)datatypes in SMT solvers ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Soundness and completeness proofs by coinductive methods ⋮ Variants of Gödel's ontological proof in a natural deduction calculus ⋮ From LTL to deterministic automata. A safraless compositional approach ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ Executable structural operational semantics in Maude ⋮ Extended feature algebra ⋮ From informal to formal proofs in Euclidean geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Formalizing Frankl’s Conjecture: FC-Families ⋮ Invariants for the FoCaL language ⋮ Flyspeck II: The basic linear programs ⋮ A compiled implementation of normalisation by evaluation ⋮ A decision procedure for linear ``big O equations ⋮ Semantics, calculi, and analysis for object-oriented specifications ⋮ A two-level logic approach to reasoning about computations ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Social choice theory in HOL. Arrow and Gibbard-Satterthwaite ⋮ Mechanized semantics for the clight subset of the C language ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ Crystal: Integrating structured queries into a tactic language ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started ⋮ Predictive runtime enforcement ⋮ Certified Kruskal’s Tree Theorem ⋮ Formalizing Probabilistic Noninterference ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface ⋮ A Verified Enclosure for the Lorenz Attractor (Rough Diamond) ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Deriving Comparators and Show Functions in Isabelle/HOL ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Taming Paraconsistent (and Other) Logics ⋮ The refinement calculus of reactive systems ⋮ Strategyproof social choice when preferences and outcomes may contain ties ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Automation for interactive proof: first prototype ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Second-order properties of undirected graphs ⋮ Relation-algebraic verification of Borůvka's minimum spanning tree algorithm ⋮ Automated reasoning for probabilistic sequential programs with theorem proving ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ A Discrete Geometric Model of Concurrent Program Execution ⋮ Towards a UTP Semantics for Modelica ⋮ A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation ⋮ SMT proof checking using a logical framework ⋮ Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book ⋮ Translating higher-order clauses to first-order clauses ⋮ Proving pointer programs in higher-order logic ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ The Expressive Power of Monotonic Parallel Composition ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ Shallow confluence of conditional term rewriting systems ⋮ Automating Soundness Proofs ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Effective Normalization Techniques for HOL ⋮ Automating Free Logic in Isabelle/HOL ⋮ Agent-Based HOL Reasoning ⋮ The GDML and EuKIM Projects: Short Report on the Initiative ⋮ An Isabelle/HOL Formalisation of Green’s Theorem ⋮ HOL Zero’s Solutions for Pollack-Inconsistency ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ Mechanical Verification of a Constructive Proof for FLP ⋮ The Flow of ODEs ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems ⋮ Automatic Functional Correctness Proofs for Functional Search Trees ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Algebraic Numbers in Isabelle/HOL ⋮ Semantic Determinism and Functional Logic Program Properties ⋮ Programmed Strategies for Program Verification ⋮ Enhancing Theorem Prover Interfaces with Program Slice Information ⋮ Web Interfaces for Proof Assistants ⋮ Tool Support for Proof Engineering ⋮ Modeling and Verifying Graph Transformations in Proof Assistants ⋮ A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle ⋮ A framework for the verification of certifying computations ⋮ Reducing higher-order theorem proving to a sequence of SAT problems ⋮ Extending Sledgehammer with SMT solvers ⋮ Proof pearl: A mechanized proof of GHC's mergesort ⋮ Expander2: Program Verification Between Interaction and Automation ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ On the fine-structure of regular algebra ⋮ Formalizing complex plane geometry ⋮ Formalizing provable anonymity in Isabelle/HOL ⋮ Concurrent Dynamic Algebra ⋮ An Assertional Proof of the Stability and Correctness of Natural Mergesort ⋮ Convolution as a Unifying Concept ⋮ Taming Multirelations ⋮ How Hard Is Positive Quantification? ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Stone Relation Algebras ⋮ Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants ⋮ Unnamed Item ⋮ Automated Kantian ethics: a faithful implementation ⋮ Specification and verification of concurrent systems by causality and realizability ⋮ Fundamentals of compositional rewriting theory ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ A formalised theorem in the partition calculus ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Machine Learning for Inductive Theorem Proving ⋮ VeriMon: a formally verified monitoring tool ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Embedded domain specific verifiers ⋮ What is the point of computers? A question for pure mathematicians ⋮ Isabelle formalisation of original representation theorems ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis ⋮ Combining higher-order logic with set theory formalizations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ \textsf{symQV}: automated symbolic verification of quantum programs ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ Verifying feedforward neural networks for classification in Isabelle/HOL ⋮ Integrating ADTs in KeY and their application to history-based reasoning about collection ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formal power series ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Binary-Compatible Verification of Filesystems with ACL2 ⋮ Refinement-Based Verification of Interactive Real-Time Systems ⋮ Experimenting Formal Proofs of Petri Nets Refinements ⋮ Reasoning About Multi-Lingual Exception Handling Using RIPLS ⋮ Analogy in Automated Deduction: A Survey ⋮ CSP-CASL-Prover: A Generic Tool for Process and Data Refinement ⋮ The Stable Revivals Model in CSP-Prover ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains ⋮ Formal Verification of Graph Grammars using Mathematical Induction ⋮ Verified Compilation and the B Method: A Proposal and a First Appraisal ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ A case-study in algebraic manipulation using mechanized reasoning tools ⋮ Binary codes that do not preserve primitivity ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} ⋮ A formal proof of the expressiveness of deep learning ⋮ Extending Sledgehammer with SMT Solvers ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ A Formalization of the C99 Standard in HOL, Isabelle and Coq ⋮ Verified analysis of random binary tree structures ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Cardinality of relations and relational approximation algorithms ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Decision Procedures for Multisets with Cardinality Constraints ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Certified Reasoning with Infinity ⋮ A comprehensive framework for saturation theorem proving ⋮ Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts ⋮ Scalable fine-grained proofs for formula processing ⋮ Efficient verified (UN)SAT certificate checking ⋮ MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY ⋮ Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? ⋮ On Correctness of Mathematical Texts from a Logical and Practical Point of View ⋮ Formalizing Scientifically Applicable Mathematics in a Definitional Framework ⋮ Proof Auditing Formalised Mathematics ⋮ A comprehensive framework for saturation theorem proving ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP ⋮ Free Theorems and Runtime Type Representations ⋮ A mechanically verified theory of contracts ⋮ Sound reasoning in \textit{tock}-CSP ⋮ Strong eventual consistency of the collaborative editing framework WOOT ⋮ Formalizing axiomatic systems for propositional logic in Isabelle/HOL ⋮ Operational semantics of the Java Card Virtual Machine ⋮ Verified bytecode verification and type-certifying compilation ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Towards finding longer proofs ⋮ A formal semantics of the GraalVM intermediate representation ⋮ A verified decision procedure for orders in Isabelle/HOL ⋮ Information-flow control on ARM and POWER multicore processors ⋮ Formalized soundness and completeness of epistemic logic ⋮ Loop verification with invariants and contracts ⋮ Generalized arrays for Stainless frames ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Empowering the Event-B method using external theories ⋮ Formalization of the resolution calculus for first-order logic ⋮ Stateful protocol composition ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ Principles of proof scores in CafeOBJ ⋮ Some general results about proof normalization ⋮ Left omega algebras and regular equations ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ A formalized general theory of syntax with bindings ⋮ Reasoning about algebraic data types with abstractions ⋮ A formally verified proof of the central limit theorem ⋮ Formally proving size optimality of sorting networks ⋮ In praise of algebra ⋮ Quantified multimodal logics in simple type theory ⋮ The locally nameless representation ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ A semantic framework for proof evidence ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Formal reasoning under cached address translation ⋮ Relational characterisations of paths ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ From types to sets by local type definition in higher-order logic ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ An assertional proof of red-black trees using Dafny ⋮ A verified proof checker for higher-order logic ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ On the semantics of polychronous polytimed specifications ⋮ Certifying emptiness of timed Büchi automata ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ Unifying theories of reactive design contracts ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ Organizing numerical theories using axiomatic type classes ⋮ A graph library for Isabelle ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ Relation algebra as programming language using the Ampersand compiler ⋮ From LCF to Isabelle/HOL ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Fifty years of Hoare's logic ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ An algebraic framework for minimum spanning tree problems ⋮ An abstract model for proving safety of autonomous urban traffic ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Automated proof of Bell-LaPadula security properties ⋮ Certifying Findel derivatives for blockchain ⋮ Formalization of function matrix theory in HOL ⋮ Certified abstract cost analysis ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Solving quantifier-free first-order constraints over finite sets and binary relations ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Verified interactive computation of definite integrals ⋮ Extending SMT solvers to higher-order logic ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Certified equational reasoning via ordered completion ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ Experiences from exporting major proof assistant libraries ⋮ Mechanized metatheory revisited ⋮ An Isabelle/HOL formalisation of Green's theorem ⋮ Model-theoretic conservative extension for definitional theories ⋮ Discovering and certifying lower bounds for the online bin stretching problem ⋮ Non-standard analysis in dynamic geometry ⋮ Interactive verification of architectural design patterns in FACTum ⋮ Term-generic logic ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Formalizing a Seligman-style tableau system for hybrid logic (short paper) ⋮ Theorem proving as constraint solving with coherent logic ⋮ A formalization of the Smith normal form in higher-order logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Infinite executions of lazy and strict computations ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Synchronization modulo \(P\) in dynamic networks ⋮ Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Mechanizing complemented lattices within Mizar type system ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Eisbach: a proof method language for Isabelle ⋮ Mechanizing a process algebra for network protocols ⋮ A heuristic prover for real inequalities ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ Balancing the load. Leveraging a semantics stack for systems verification ⋮ An algebraic approach to computations with progress ⋮ Developments in concurrent Kleene algebra ⋮ Proof pearl: Mechanizing the textbook proof of Huffman's algorithm ⋮ Formalization and implementation of modern SAT solvers ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Nominal unification with atom-variables ⋮ Cones and foci: A mechanical framework for protocol verification ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Mathematical method and proof ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Verifying the SET purchase protocols ⋮ Formal analysis of multiparty contract signing ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Supporting the formal verification of mathematical texts ⋮ Security types preserving compilation ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ A verified ODE solver and the Lorenz attractor ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Verified iptables firewall analysis and verification ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Verifying a signature architecture: a comparative case study ⋮ And so on \dots : reasoning with infinite diagrams ⋮ Verification of FPGA layout generators in higher-order logic ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving ⋮ Trace-based verification of imperative programs with I/O ⋮ Tactics for hierarchical proof ⋮ A condensed semantics for qualitative spatial reasoning about oriented straight line segments ⋮ Certifying compilers using higher-order theorem provers as certificate checkers ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps ⋮ Invariant diagrams with data refinement ⋮ ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Combining decision procedures by (model-)equality propagation ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Conjecture synthesis for inductive theories ⋮ Monotonicity inference for higher-order formulas ⋮ Analytic tableaux for higher-order logic with choice ⋮ Decreasing diagrams and relative termination ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Verification conditions for source-level imperative programs ⋮ Representing model theory in a type-theoretical logical framework ⋮ An inductive approach to strand spaces ⋮ On theorem prover-based testing ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ A mechanized proof of the basic perturbation lemma ⋮ Rewriting with equivalence relations in ACL2 ⋮ Nominal techniques in Isabelle/HOL ⋮ Recycling proof patterns in Coq: case studies ⋮ Verification and code generation for invariant diagrams in Isabelle ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Amortized complexity verified ⋮ Proof synthesis and reflection for linear arithmetic ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ Computer-assisted analysis of the Anderson-Hájek ontological controversy ⋮ A framework for developing stand-alone certifiers ⋮ Partial order semantics for use case and task models ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ The axiomatization of override and update ⋮ Reachability analysis over term rewriting systems ⋮ Linear quantifier elimination ⋮ A revision of the proof of the Kepler conjecture ⋮ Relational bytecode correlations ⋮ Frame rule for mutually recursive procedures manipulating pointers ⋮ Building program construction and verification tools from algebraic principles ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Test-data generation for control coverage by proof ⋮ HasCasl: integrated higher-order specification and program development ⋮ Integrating external deduction tools with ACL2 ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ The RISC ProofNavigator: a proving assistant for program verification in the classroom ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ Adapting functional programs to higher order logic ⋮ Analysis of a clock synchronization protocol for wireless sensor networks ⋮ Inductive proof search modulo ⋮ Operating system verification---an overview ⋮ An extensible encoding of object-oriented data models in HOL. With an application to IMP++ ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS ⋮ The future of logic: foundation-independence ⋮ ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Verified Certification of Reachability Checking for Timed Automata ⋮ Mechanical proofs about BW multi-party contract signing protocol ⋮ Unnamed Item ⋮ A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper) ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation ⋮ Verification of Closest Pair of Points Algorithms ⋮ Ernst-Rüdiger Olderog: A Life for Meaning ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Expressing Polymorphic Types in a Many-Sorted Language ⋮ Generalized and Formalized Uncurrying ⋮ Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Automating Change of Representation for Proofs in Discrete Mathematics ⋮ Introduction to Model Checking ⋮ Combining Model Checking and Deduction ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ SEPIA: Search for Proofs Using Inferred Automata ⋮ KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems ⋮ Verified Root-Balanced Trees ⋮ The Role of Indirections in Lazy Natural Semantics ⋮ Extracting a DPLL Algorithm ⋮ The Logic of U ·(TP)2 ⋮ Higher-Order UTP for a Theory of Methods ⋮ Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm ⋮ Specifying Properties of Dynamic Architectures Using Configuration Traces ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Formal Certification of a Resource-Aware Language Implementation ⋮ Liveness Reasoning with Isabelle/HOL ⋮ Generalized Theoroidal Institution Comorphisms ⋮ Heterogeneous Logical Environments for Distributed Specifications ⋮ Interacting with Modal Logics in the Coq Proof Assistant ⋮ Refinement-Based Verification of Communicating Unstructured Code ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ Interactive and automated proofs for graph transformations ⋮ Verified Construction of Fair Voting Rules ⋮ Unnamed Item ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Computer-Supported Exploration of a Categorical Axiomatization of Modeloids ⋮ Computer-Supported Analysis of Arguments in Climate Engineering ⋮ LOGICS OF FORMAL INCONSISTENCY ENRICHED WITH REPLACEMENT: AN ALGEBRAIC AND MODAL ACCOUNT ⋮ The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification ⋮ Extending a Resolution Prover for Inequalities on Elementary Functions ⋮ Constraint solving for finite model finding in SMT solvers ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ UTPCalc — A Calculator for UTP Predicates ⋮ Unnamed Item ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument ⋮ Unnamed Item ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ Friends with Benefits ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Preservation of Proof Obligations from Java to the Java Virtual Machine ⋮ Efficient Well-Definedness Checking ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ Data Refinement of Invariant Based Programs ⋮ Guarded Operations, Refinement and Simulation ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Proof Verification Technology and Elementary Physics ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ Verification of the Schorr-Waite Algorithm – From Trees to Graphs ⋮ Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments ⋮ Hoare Semigroups ⋮ Fixpoints and Search in PVS ⋮ Applicable Mathematics in a Minimal Computational Theory of Sets ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ Unbounded Discrepancy of Deterministic Random Walks on Grids ⋮ Pollack-inconsistency ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ Termination Graphs for Java Bytecode ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) ⋮ Second-Order Programs with Preconditions ⋮ Unnamed Item ⋮ From a Proven Correct Microkernel to Trustworthy Large Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Logical Formalisation and Analysis of the Mifare Classic Card in PVS ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism ⋮ Local Theory Specifications in Isabelle/Isar ⋮ Using Structural Recursion for Corecursion ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Algebra of Monotonic Boolean Transformers ⋮ A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell* ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Cogent: uniqueness types and certifying compilation ⋮ Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi

Uses Software