scientific article; zbMATH DE number 1424012
From MaRDI portal
Publication:4945200
Recommendations
- The \(HOL\) logic extended with quantification over type variables
- scientific article; zbMATH DE number 2185691
- scientific article; zbMATH DE number 234014
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
Cited in
(25)- HasCasl: integrated higher-order specification and program development
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- A formalized general theory of syntax with bindings
- A formalized general theory of syntax with bindings: extended version
- scientific article; zbMATH DE number 1617310 (Why is no real title available?)
- A first-order syntax for the -calculus in Isabelle/HOL using permutations
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Comprehending Isabelle/HOL’s Consistency
- scientific article; zbMATH DE number 2185691 (Why is no real title available?)
- The HOL-Omega Logic
- A Purely Definitional Universal Domain
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- The Isabelle Framework
- Monotonicity inference for higher-order formulas
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- Architectural_Design_Patterns
- Monotonicity inference for higher-order formulas
- SSCalc: a calculus for Solidity smart contracts
- Type safety for Isabelle/Solidity
- Type safety for Isabelle/Solidity
- Inductive predicates via least fixpoints in higher-order separation logic
- The HOL-CSP Refinement Toolkit
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- Partial and nested recursive function definitions in higher-order logic
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 Q4945200)
