skip to main content
10.1145/2676726.2676974acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Programming up to Congruence

Published: 14 January 2015 Publication History

Abstract

This paper presents the design of Zombie, a dependently-typed programming language that uses an adaptation of a congruence closure algorithm for proof and type inference. This algorithm allows the type checker to automatically use equality assumptions from the context when reasoning about equality. Most dependently-typed languages automatically use equalities that follow from beta-reduction during type checking; however, such reasoning is incompatible with congruence closure. In contrast, Zombie does not use automatic beta-reduction because types may contain potentially diverging terms. Therefore Zombie provides a unique opportunity to explore an alternative definition of equivalence in dependently-typed language design.
Our work includes the specification of the language via a bidirectional type system, which works "up-to-congruence,'' and an algorithm for elaborating expressions in this language to an explicitly typed core language. We prove that our elaboration algorithm is complete with respect to the source type system, and always produces well typed terms in the core language. This algorithm has been implemented in the Zombie language, which includes general recursion, irrelevant arguments, heterogeneous equality and datatypes.

Supplementary Material

MPG File (p369-sidebyside.mpg)

References

[1]
T. Altenkirch. The case of the smart case: How to implement conditional convertibility? Presentation at NII Shonan seminar 007, Japan, Sept. 2011.
[2]
T. Altenkirch, C. McBride, and W. Swierstra. Observational equality, now! In PLPV '07: Programming Languages meets Program Verification, pages 57--68. ACM, 2007.
[3]
L. Augustsson. Cayenne -- a language with dependent types. In ICFP '98: International Conference on Functional Programming, pages 239--250. ACM, 1998.
[4]
L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion Without Failure. In A. H. Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2: Rewriting Techniques, pages 1--30. Academic Press, 1989.
[5]
B. Barras and B. Bernardo. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In 11th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2008), volume 4962 of LNCS, pages 365--379. Springer, 2008.
[6]
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
[7]
G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic subtyping with an SMT solver. In ICFP '10: International Conference on Functional Programming, pages 105--116, 2010.
[8]
E. C. Brady. Idris-systems programming meets full dependent types. In PLPV'11: Programming languages meets program verification, pages 43--54. ACM, 2011. ISBN 978--1--4503-0487-0.
[9]
C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and programs in a dependently typed langauge. In POPL '14: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014.
[10]
P. Corbineau. Deciding equality in the constructor theory. In T. Altenkirch and C. McBride, editors, Types for Proofs and Programs, volume 4502 of Lecture Notes in Computer Science, pages 78--92. Springer Berlin Heidelberg, 2007.
[11]
K. Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, 1998.
[12]
L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, pages 337--340, Berlin, Heidelberg, 2008. Springer-Verlag.
[13]
L. de Moura, H. Rueß, and N. Shankar. Justifying equality. Electronic Notes in Theoretical Computer Science (ENTCS), 125 (3): 69--85, July 2005.
[14]
P. J. Downey, R. Sethi, and R. E. Tarjan. Variations on the common subexpression problem. J. ACM, 27 (4): 758--771, Oct. 1980.
[15]
J. Gallier, W. Snyder, P. Narendran, and D. Plaisted. Rigid E-unification is NP-complete. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), pages 218--227, 1988.
[16]
L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. AURA: A programming language for authorization and audit. In ICFP '08: International Conference on Functional Programming), pages 27--38, 2008.
[17]
K. R. M. Leino. Dafny: an automatic program verifier for functional correctness. In Proceedings of the 16th international conference on Logic for programming, artificial intelligence, and reasoning, LPAR'10, pages 348--370. Springer-Verlag, 2010.
[18]
C. McBride. First-order unification by structural recursion, 2001.
[19]
G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27 (2): 356--364, Apr. 1980.
[20]
R. Nieuwenhuis and A. Oliveras. Fast congruence closure and extensions. Inf. Comput., 205 (4): 557--580, Apr. 2007.
[21]
A. Petcher and A. Stump. Deciding Joinability Modulo Ground Equations in Operational Type Theory. In S. Lengrand and D. Miller, editors, Proof Search in Type Theories (PSTT), 2009.
[22]
B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22 (1): 1--44, Jan. 2000.
[23]
P. Sewell, F. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strnisa. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20 (1): 71--122, 2010.
[24]
R. E. Shostak. An algorithm for reasoning about equality. Commun. ACM, 21 (7): 583--585, July 1978.
[25]
V. Sjöberg and S. Weirich. Programming up to congruence (extended version). Technical Report MS-CIS-14--10, University of Pennsylvania, Philadelphia, PA, Oct. 2014.
[26]
V. Sjöberg, C. Casinghino, K. Y. Ahn, N. Collins, H. D. Eades III, P. Fu, G. Kimmell, T. Sheard, A. Stump, and S. Weirich. Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In J. Chapman and P. B. Levy, editors, MSFP '12, volume 76 of EPTCS, pages 112--162. Open Publishing Association, 2012.
[27]
A. Stampoulis and Z. Shao. Static and user-extensible proof checking. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 273--284, New York, NY, USA, 2012. ACM.
[28]
P.-Y. Strub. Coq modulo theory. In CSL, pages 529--543, 2010.
[29]
A. Stump and L.-Y. Tan. The algebra of equality proofs. In 16th International Conference on Rewriting Techniques and Applications (RTA'05), pages 469--483. Springer, 2005.
[30]
N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure Distributed Programming with Value-dependent Types. In ICFP '11: International Conference on Functional Programming, pages 285--296. ACM, 2011.

Cited By

View all
  • (2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
  • (2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
  • (2022)Oblivious algebraic data typesProceedings of the ACM on Programming Languages10.1145/34987136:POPL(1-29)Online publication date: 12-Jan-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
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 the author(s) 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].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. congruence closure
  2. dependent types

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)14
  • Downloads (Last 6 weeks)2
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
  • (2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
  • (2022)Oblivious algebraic data typesProceedings of the ACM on Programming Languages10.1145/34987136:POPL(1-29)Online publication date: 12-Jan-2022
  • (2021)Congruence Closure Modulo Permutation EquationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.342.8342(86-98)Online publication date: 6-Sep-2021
  • (2021)Bidirectional TypingACM Computing Surveys10.1145/345095254:5(1-38)Online publication date: 25-May-2021
  • (2019)Pure iso-type systemsJournal of Functional Programming10.1017/S095679681900010829Online publication date: 17-Sep-2019
  • (2017)Refinement reflection: complete verification with SMTProceedings of the ACM on Programming Languages10.1145/31581412:POPL(1-31)Online publication date: 27-Dec-2017
  • (2017)Unifying typing and subtypingProceedings of the ACM on Programming Languages10.1145/31338711:OOPSLA(1-26)Online publication date: 12-Oct-2017
  • (2017)A specification for dependent types in HaskellProceedings of the ACM on Programming Languages10.1145/31102751:ICFP(1-29)Online publication date: 29-Aug-2017
  • (2017)Local refinement typingProceedings of the ACM on Programming Languages10.1145/31102701:ICFP(1-27)Online publication date: 29-Aug-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media