The exp-log normal form of types: decomposing extensional equality and representing terms compactly

DOI10.1145/3009837.3009841zbMath1380.68093arXiv1502.04634OpenAlexW3102609340MaRDI QIDQ5370876

Danko Ilik

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

type-directed partial evaluationsum typetype isomorphismnormal typeeta-equalitynormal term

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (2)

An intuitionistic formula hierarchy based on high‐school identities ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Uses Software

• Coq

This page was built for publication: The exp-log normal form of types: decomposing extensional equality and representing terms compactly