article

A syntactic approach to eta equality in type theory

Author:

Healfdene GoguenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 75 - 84

https://doi.org/10.1145/1047659.1040312

Published: 12 January 2005 Publication History

Abstract

This paper outlines an elementary approach for showing the decidability of type checking for type theories with βη-equality, relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic translation mapping terms in the βη presentation into their full η-expansions in the β presentation. Decidability of type checking is lifted from the target β presentation to the βη presentation. The approach extends to other inductive kinds with a single constructor, and is demonstrated for singletons and dependent pairs.

References

[1]

M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375--416, 1991.

[2]

G. Barthe. Existence and uniqueness of normal forms in pure type systems with beta-eta conversion. In Proceedings of Computer Science Logic, CSL'98, volume 1584 of Lecture Notes in Computer Science, pages 241--259. Springer--Verlag, 1998.

Digital Library

[3]

A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. A later version is published as {4}.

[4]

A. Compagnoni and H. Goguen. Typed operational semantics for higher-order subtyping. Information and Computation, 184(2):242--297, Aug. 2003.

Digital Library

[5]

T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

Digital Library

[6]

T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. Extended version of {7}, 2003.

[7]

T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. In Proceedings of Typed Lambda Calculus and Applications, TLCA'03, volume 2701 of Lecture Notes in Computer Science. Springer-Verlag, 2003. See extended version {6}.

Digital Library

[8]

R. D. Cosmo and D. Kesner. A confluent reduction system for the extensional typed lambda-calculus with pairs, sum, recursion and terminal object. In Proceedings of the 20st International Colloquium on Automata, Languages and Programming (ICALP'93), volume 700 of Lecture Notes in Computer Science, pages 645--656. Springer--Verlag, July 1993.

Digital Library

[9]

G. Dowek, G. Huet, and B. Werner. On the definition of the eta-long normal form in type systems of the cube. In Informal Proceedings of the Workshop on Types for Proofs and Programs, 1993.

[10]

H. Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, Sept. 1993.

[11]

N. Ghani. Eta-expansions in dependent type theory - the calculus of constructions. In Typed Lambda Calculus and Applications, volume 1210 of Lecture Notes in Computer Science, pages 164--180. Springer--Verlag, 1997.

Digital Library

[12]

H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994.

[13]

H. Goguen. A Kripke-style model for the admissibility of structural rules. In Proceedings of TYPES, volume 2277 of Lecture Notes in Computer Science, pages 112--124. Springer--Verlag, 2000.

Digital Library

[14]

H. Goguen. Justifying algorithms for beta-eta conversion. 2004. Submitted to FOSSACS 2005.

Digital Library

[15]

R. Harper and F. Pfenning. On equivalence and canonical forms in the LF type theory. ACM Trans. on Computational Logic, 2003. (To appear).

Digital Library

[16]

F. Joachimski. Syntactic analysis of eta-expansions in pure type systems. Information and Computation, 182(1):53--71, 2003.

Digital Library

[17]

J. W. Klop. Combinatory reduction systems. Mathematical Centre Tracts 127, Centre for Mathematics and Computer Science, Amsterdam, 1980. PhD thesis.

[18]

J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics. Cambridge University Press, 1989.

Digital Library

[19]

Z. Luo. Computation and Reasoning. Oxford University Press, 1994.

Digital Library

[20]

D. MacQueen. Using dependent types to express modular structure. In Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, 1986.

Digital Library

[21]

A. Salvesen. The Church-Rosser property for pure type systems with βη-reduction, Nov. 1991. Unpublished manuscript.

[22]

C. A. Stone and R. Harper. Equivalence and singletons. ACM Transactions on Programming Languages and Systems, 2004. Submitted.

[23]

T. Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkhäuser, 1991.

Digital Library

[24]

B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Université Paris 7, 1994.

Cited By

Lennon-Bertrand MMaillard KTabareau NTanter É(2022)Gradualizing the Calculus of Inductive ConstructionsACM Transactions on Programming Languages and Systems10.1145/349552844:2(1-82)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3495528
Coquand TPollack RTakeyama M(2019)A Logical Framework with Dependently Typed RecordsFundamenta Informaticae10.5555/2370077.237008365:1-2(113-134)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/2370077.2370083
Abel ACoquand T(2019)Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective PairsFundamenta Informaticae10.5555/2366462.236646777:4(345-395)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/2366462.2366467
Show More Cited By

Index Terms

A syntactic approach to eta equality in type theory
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus

Recommendations

A syntactic approach to eta equality in type theory
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This paper outlines an elementary approach for showing the decidability of type checking for type theories with βη-equality, relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Type checking and typability in domain-free lambda calculi

This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
442
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lennon-Bertrand MMaillard KTabareau NTanter É(2022)Gradualizing the Calculus of Inductive ConstructionsACM Transactions on Programming Languages and Systems10.1145/349552844:2(1-82)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3495528
Coquand TPollack RTakeyama M(2019)A Logical Framework with Dependently Typed RecordsFundamenta Informaticae10.5555/2370077.237008365:1-2(113-134)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/2370077.2370083
Abel ACoquand T(2019)Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective PairsFundamenta Informaticae10.5555/2366462.236646777:4(345-395)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/2366462.2366467
Abel ACoquand T(2019)Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective PairsFundamenta Informaticae10.5555/1365997.136600277:4(345-395)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/1365997.1366002
Coquand TPollack RTakeyama M(2019)A Logical Framework with Dependently Typed RecordsFundamenta Informaticae10.5555/1227143.122714965:1-2(113-134)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.5555/1227143.1227149
Abel ACoquand TPagano M(2011)A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof IrrelevanceLogical Methods in Computer Science10.2168/LMCS-7(2:4)20117:2Online publication date: 7-May-2011
https://doi.org/10.2168/LMCS-7(2:4)2011
Urban CCheney JBerghofer S(2011)Mechanizing the metatheory of LFACM Transactions on Computational Logic (TOCL)10.1145/1877714.187772112:2(1-42)Online publication date: 27-Jan-2011
https://dl.acm.org/doi/10.1145/1877714.1877721
Urban CCheney JBerghofer S(2008)Mechanizing the Metatheory of LFProceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.2008.29(45-56)Online publication date: 24-Jun-2008
https://dl.acm.org/doi/10.1109/LICS.2008.29
Westbrook EStump AWehrman I(2005)A language-based approach to functionally correct imperative programmingACM SIGPLAN Notices10.1145/1090189.108640040:9(268-279)Online publication date: 12-Sep-2005
https://dl.acm.org/doi/10.1145/1090189.1086400
Westbrook EStump AWehrman IDanvy OPierce B(2005)A language-based approach to functionally correct imperative programmingProceedings of the tenth ACM SIGPLAN international conference on Functional programming10.1145/1086365.1086400(268-279)Online publication date: 28-Sep-2005
https://dl.acm.org/doi/10.1145/1086365.1086400
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents