Modular dependent induction in Coq, Mendler-style

DOI10.1007/978-3-319-43144-4_25MaRDI QIDQ2829276zbMATH OpenOpenAlexFDO

Authors Paolo Torrini

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Reasoning about modular datatypes with Mendler induction
• Efficient Mendler-style lambda-encodings in Cedille
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• Meta-theory à la carte
• Truly modular (co)datatypes for Isabelle/HOL

Cites work

• scientific article; zbMATH DE number 1400097 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences
• A tutorial on the universality and expressiveness of fold
• Containers: Constructing strictly positive types
• Data types à la carte
• Inductive types and type constraints in the second-order lambda calculus
• Iteration and coiteration schemes for higher-order and nested datatypes
• Map fusion for nested datatypes in intensional type theory
• Meta-theory à la carte
• Modular dependent induction in Coq, Mendler-style
• Modular monadic meta-theory
• The calculus of constructions
• Type-based termination of generic programs

Cited in

(6)

• Modular dependent induction in Coq, Mendler-style
• Tactics for Reasoning Modulo AC in Coq
• Reasoning about modular datatypes with Mendler induction
• Meta-theory à la carte
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• Efficient Mendler-style lambda-encodings in Cedille

Describes a project that uses

Uses Software

• Coq
• Agda

This page was built for publication: Modular dependent induction in Coq, Mendler-style

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829276)