αCheck: A mechanized metatheory model checker
From MaRDI portal
Publication:4593089
DOI10.1017/S1471068417000035zbMath1379.68236arXiv1704.00617MaRDI QIDQ4593089
Alberto Momigliano, James Cheney
Publication date: 9 November 2017
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1704.00617
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (5)
Unnamed Item ⋮ Towards substructural property-based testing ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Nominal unification with letrec and environment-variables
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Tests and proofs. 10th international conference, TAP 2016, held as part of STAF 2016, Vienna, Austria, July 5--7, 2016. Proceedings
- Equivariant unification
- A new approach to abstract syntax with variable binding
- Verifying termination and reduction properties about higher-order logic programs
- About permutation algebras, (pre)sheaves and named sets
- A polynomial nominal unification algorithm
- An overview of the K semantic framework
- Explicit representation of terms defined by counter examples
- Orienting rewrite rules with the Knuth-Bendix order.
- Nominal unification
- Negation and constraint logic programming
- Fresh logic: Proof-theory and semantics for FM and nominal techniques
- A two-level logic approach to reasoning about computations
- Functional and logic programming. 12th international symposium, FLOPS 2014, Kanazawa, Japan, June 4--6, 2014. Proceedings
- Uniform proofs as a foundation for logic programming
- Nominal Sets
- Smart Testing of Functional Programs in Isabelle
- Concrete Semantics
- Scrap your nameplate
- Causal commutative arrows and their optimization
- Foundational Property-Based Testing
- Proof search specifications of bisimulation and modal logics for the π-calculus
- Mechanizing the metatheory of LF
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
- Automatic Proof and Disproof in Isabelle/HOL
- The Twelf Proof Assistant
- Answer Set Programming: A Declarative Approach to Solving Search Problems
- Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
- Success and failure for hereditary Harrop formulae
- Logic programming and negation: A survey
- Constraint Logic Programming with Hereditary Harrop formulas
- A transformational approach to negation in logic programming
- The New Quickcheck for Isabelle
- Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
- Binders unbound
- Ott: Effective tool support for the working semanticist
- Higher-order pattern complement and the strict λ-calculus
- On equivalence and canonical forms in the LF type theory
- Functional and Logic Programming
- An Efficient Nominal Unification Algorithm
- Completeness and Herbrand theorems for nominal logic
- Theorem Proving in Higher Order Logics
- Static typing for a faulty lambda calculus
- A simple sequent calculus for nominal logic
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Nominal Unification from a Higher-Order Perspective
This page was built for publication: αCheck: A mechanized metatheory model checker
