Reasoning about modular datatypes with Mendler induction

zbMATH Open1476.68056arXiv1509.03021MaRDI QIDQ5014449FDOQ5014449

Authors: Paolo Torrini, Tom Schrijvers 

Publication date: 2 December 2021

Full work available at URL: https://arxiv.org/abs/1509.03021

Recommendations

• Modular dependent induction in Coq, Mendler-style
• Efficient Mendler-style lambda-encodings in Cedille
• Meta-theory à la carte
• Publication:4939621
• A type-theoretic approach to induction with higher-order encodings

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cites Work

• Ott: Effective tool support for the working semanticist
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A tutorial on the universality and expressiveness of fold
• The calculus of constructions
• The origins of structural operational semantics
• Iteration and coiteration schemes for higher-order and nested datatypes
• Inductive types and type constraints in the second-order lambda calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Data types à la carte
• Programming Languages and Systems
• Inductively defined types in the Calculus of Constructions
• Meta-theory à la carte
• Modular monadic meta-theory

Cited In (6)

• A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences
• Modularity of proof-nets. Generating the type of a module.
• Modular dependent induction in Coq, Mendler-style
• Title not available (Why is that?)
• Efficient Mendler-style lambda-encodings in Cedille
• Title not available (Why is that?)

Uses Software

• Coq
• Automath

This page was built for publication: Reasoning about modular datatypes with Mendler induction

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