A syntactic approach to eta equality in type theory

DOI10.1145/1040305.1040312zbMath1369.68137OpenAlexW2020660597MaRDI QIDQ5276136

Healfdene Goguen

Publication date: 14 July 2017

Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1040305.1040312

zbMATH Keywords

decidabilitylogical frameworkstype checkingbeta-eta equality

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (1)

The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

This page was built for publication: A syntactic approach to eta equality in type theory