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