skip to main content
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

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. congruence closure
  2. dependent types

Qualifiers

  • Research-article

Funding Sources

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
  • (2023)Explicit Refinement TypesProceedings of the ACM on Programming Languages10.1145/36078377:ICFP(187-214)Online publication date: 30-Aug-2023
  • (2016)Unified Syntax with Iso-typesProgramming Languages and Systems10.1007/978-3-319-47958-3_14(251-270)Online publication date: 9-Oct-2016
  • (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
  • 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