Efficiency of lambda-encodings in total type theory

DOI10.1017/S0956796816000034zbMath1420.68045MaRDI QIDQ5371961

Peng Fu, Aaron Stump

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Related Items (3)

From realizability to induction via dependent intersection ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ The calculus of dependent lambda eliminations

Uses Software

• Coq
• PLT Redex
• Racket

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Combinatory logic. Vol. II
• Three algorithms on Braun trees
• THEORETICAL PEARL Church numerals, twice!
• Self Types for Dependently Typed Lambda Encodings
• Computer Science Logic

This page was built for publication: Efficiency of lambda-encodings in total type theory