Modular dependent induction in Coq, Mendler-style

DOI10.1007/978-3-319-43144-4_25zbMATH Open1478.68438OpenAlexW2501836004MaRDI QIDQ2829276FDOQ2829276

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

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

Mathematics Subject Classification ID

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

Cites Work

• Containers: Constructing strictly positive types
• A tutorial on the universality and expressiveness of fold
• The calculus of constructions
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Iteration and coiteration schemes for higher-order and nested datatypes
• Map fusion for nested datatypes in intensional type theory
• Inductive types and type constraints in the second-order lambda calculus
• Title not available (Why is that?)
• Data types à la carte
• Type-based termination of generic programs
• A hierarchy of mendler style recursion combinators
• Modular Dependent Induction in Coq, Mendler-Style
• Meta-theory à la carte
• Modular monadic meta-theory

Cited In (2)

• Tactics for Reasoning Modulo AC in Coq
• Modular Dependent Induction in Coq, Mendler-Style

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)