scientific article; zbMATH DE number 7204430
From MaRDI portal
Publication:5111307
Recommendations
- Isabelle formalization of set theoretic structures and set comprehensions
- Hereditarily finite sets in constructive type theory
- Multisets in type theory
- Nested sequents for intuitionistic logics
- Higher-order abstract syntax in Isabelle/HOL
- Isabelle/HOL/GST: a formal proof environment for generalized set theories
- Multitraces, hypertraces and partial order semantics
- Hierarchies of monadic generalized quantifiers
- Higher-order separation logic in Isabelle/HOLCF
- scientific article; zbMATH DE number 58733
Cites work
- scientific article; zbMATH DE number 3136760 (Why is no real title available?)
- scientific article; zbMATH DE number 4114622 (Why is no real title available?)
- scientific article; zbMATH DE number 1889386 (Why is no real title available?)
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- A Lambda-Free Higher-Order Recursive Path Order
- A mechanizable first-order theory of ordinals
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Accessible Independence Results for Peano Arithmetic
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
- Building Formal Method Tools in the Isabelle/Isar Framework
- Cardinals in Isabelle/HOL
- Certification of Automated Termination Proofs
- Certified Size-Change Termination
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Decidability of behavioural equivalence in unary PCF
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- General bindings and alpha-equivalence in Nominal Isabelle
- Generalised multisets for chemical programming
- Isabelle/HOL. A proof assistant for higher-order logic
- LCF considered as a programming language
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- On the formalization of termination techniques based on multiset orderings
- On the restricted ordinal theorem
- Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
- Partial Recursive Functions in Higher-Order Logic
- Proving termination with multiset orderings
- Resolution theorem proving
- Setoids in type theory
- The Hydra Battle Revisited
- Truly modular (co)datatypes for Isabelle/HOL
- Unary PCF is decidable
Cited in
(6)- Formalizing ordinal partition relations using Isabelle/HOL
- Cardinals in Isabelle/HOL
- Type-theoretic approaches to ordinals
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- An alternative proof of the well-foundedness of the nested multiset ordering
Describes a project that uses
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111307)
