Inductive predicates via least fixpoints in higher-order separation logic
From MaRDI portal
Cites work
- A fixedpoint approach to implementing (co)inductive definitions
- A higher-order logic for concurrent termination-preserving refinement
- A lattice-theoretical fixpoint theorem and its applications
- A new look at generalized rewriting in type theory
- A semantics for concurrent separation logic
- A very modal model of a modern, major, general type system
- Charge! A framework for higher-order separation logic in Coq
- ELPI: fast, embeddable, Prolog interpreter
- First-Class Type Classes
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- Higher-order ghost state
- scientific article; zbMATH DE number 2185691 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 2006660 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 1424012 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- scientific article; zbMATH DE number 7649978 (Why is no real title available?)
- Inductively defined types in the Calculus of Constructions
- Interactive proofs in higher-order concurrent separation logic
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Least and greatest fixed points in linear logic
- Program verification through characteristic formulae
- Reflexive tactics for algebra, revisited
- Resources, concurrency, and local reasoning
- The calculus of constructions
- The essence of higher-order concurrent separation logic
- The Logic of Bunched Implications
- The Mechanical Evaluation of Expressions
- Time credits and time receipts in Iris
- Un théorème sur les fonctions d'ensembles.
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- VST-Floyd: a separation logic tool to verify correctness of C programs
This page was built for publication: Inductive predicates via least fixpoints in higher-order separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323681)
