A syntactic approach to eta equality in type theory

DOI10.1145/1040305.1040312MaRDI QIDQ5276136zbMATHOpenAlexFDO

Authors 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

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

Cited in

(2)

• \(\eta\)-equivalence in core dependent Haskell
• 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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5276136)