A new look at generalized rewriting in type theory
From MaRDI portal
(Redirected from Publication:3075239)
Recommendations
Cited in
(27)- Rewrite systems on a lattice of types
- Type introduction for equational rewriting
- Formalization of the arithmetization of Euclidean plane geometry and applications
- A formal C memory model for separation logic
- External rewriting for skeptical proof assistants
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Automating change of representation for proofs in discrete mathematics (extended version)
- Cardinalities of Finite Relations in Coq
- Completeness and decidability results for CTL in constructive type theory
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Foundational property-based testing
- A lightweight approach to datatype-generic rewriting
- Towards Rewriting in Coq
- scientific article; zbMATH DE number 4126684 (Why is no real title available?)
- scientific article; zbMATH DE number 1498422 (Why is no real title available?)
- Generalizing Def and Pos to Type Analysis
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- scientific article; zbMATH DE number 2085176 (Why is no real title available?)
- scientific article; zbMATH DE number 827981 (Why is no real title available?)
- Introduction to generalized type systems
- Extensional equality preservation and verified generic programming
- Quotients of bounded natural functors
- Quotients of Bounded Natural Functors
- Computer Certified Efficient Exact Reals in Coq
- A formal proof of the irrationality of (3)
- Types for Proofs and Programs
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
This page was built for publication: A new look at generalized rewriting in type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075239)
