A syntactic approach to eta equality in type theory

DOI10.1145/1040305.1040312zbMATH Open1369.68137OpenAlexW2020660597MaRDI QIDQ5276136FDOQ5276136

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

Recommendations

• scientific article; zbMATH DE number 1342216
• scientific article; zbMATH DE number 1705161
• scientific article; zbMATH DE number 2185660
• scientific article; zbMATH DE number 2185714
• scientific article; zbMATH DE number 814613

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)

• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• \(\eta\)-equivalence in core dependent Haskell

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)