Modular Dependent Induction in Coq, Mendler-Style
From MaRDI portal
Publication:2829276
DOI10.1007/978-3-319-43144-4_25zbMath1478.68438OpenAlexW2501836004MaRDI QIDQ2829276
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_25
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Map fusion for nested datatypes in intensional type theory
- Type-based termination of generic programs
- The calculus of constructions
- Iteration and coiteration schemes for higher-order and nested datatypes
- Containers: Constructing strictly positive types
- Inductive types and type constraints in the second-order lambda calculus
- Modular Dependent Induction in Coq, Mendler-Style
- Meta-theory à la carte
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Data types à la carte
- A tutorial on the universality and expressiveness of fold
- A hierarchy of mendler style recursion combinators
- Modular monadic meta-theory
This page was built for publication: Modular Dependent Induction in Coq, Mendler-Style
