A new look at generalized rewriting in type theory
From MaRDI portal
Publication:3075239
zbMATH Open1205.68364MaRDI QIDQ3075239FDOQ3075239
Publication date: 10 February 2011
Full work available at URL: http://jfr.cib.unibo.it/article/view/1574
Recommendations
Cited In (26)
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Extensional equality preservation and verified generic programming
- Title not available (Why is that?)
- Towards Rewriting in Coq
- Title not available (Why is that?)
- Types for Proofs and Programs
- Foundational Property-Based Testing
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Completeness and decidability results for CTL in constructive type theory
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- Automating change of representation for proofs in discrete mathematics (extended version)
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Computer Certified Efficient Exact Reals in Coq
- Title not available (Why is that?)
- External rewriting for skeptical proof assistants
- Quotients of Bounded Natural Functors
- Type introduction for equational rewriting
- Rewrite systems on a lattice of types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Cardinalities of Finite Relations in Coq
- A formal C memory model for separation logic
- Introduction to generalized type systems
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Generalizing Def and Pos to Type Analysis
Uses Software
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)
