Efficient Mendler-style lambda-encodings in Cedille

DOI10.1007/978-3-319-94821-8_14OpenAlexW2962695160MaRDI QIDQ1791163

Richard Blair, Aaron Stump, Denis Firsov

Publication date: 4 October 2018

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

zbMATH Keywords

type theoryinduction principleinductive datatypespredecessor functionCedillelambda-encodings

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (4)

From realizability to induction via dependent intersection ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Quotients by Idempotent Functions in Cedille ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Efficient Mendler-style lambda-encodings in Cedille