Reasoning about modular datatypes with Mendler induction

MaRDI QIDQ5014449zbMATH OpenFDO

Authors Paolo Torrini, Tom Schrijvers

Publication date 2 December 2021

Full work available at URL https://arxiv.org/abs/1509.03021, http://eptcs.web.cse.unsw.edu.au/paper.cgi?FICS2015.13

Mathematics Subject Classification ID

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

Recommendations

• Modular dependent induction in Coq, Mendler-style
• Efficient Mendler-style lambda-encodings in Cedille
• Meta-theory à la carte
• scientific article; zbMATH DE number 1400097
• A type-theoretic approach to induction with higher-order encodings

Cites work

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

Cited in

(6)

• Modularity of proof-nets. Generating the type of a module.
• Efficient Mendler-style lambda-encodings in Cedille
• scientific article; zbMATH DE number 1696611 (Why is no real title available?)
• Modular dependent induction in Coq, Mendler-style
• scientific article; zbMATH DE number 1400097 (Why is no real title available?)
• A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences

Describes a project that uses

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)