research-article

Open access

Transfinite step-indexing for termination

Authors:

Neel Krishnaswami,

Derek DreyerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 13, Pages 1 - 29

https://doi.org/10.1145/3434294

Published: 04 January 2021 Publication History

Abstract

Step-indexed logical relations are an extremely useful technique for building operational-semantics-based models and program logics for realistic, richly-typed programming languages. They have proven to be indispensable for modeling features like higher-order state, which many languages support but which were difficult to accommodate using traditional denotational models. However, the conventional wisdom is that, because they only support reasoning about finite traces of computation, (unary) step-indexed models are only good for proving safety properties like “well-typed programs don’t go wrong”. There has consequently been very little work on using step-indexing to establish liveness properties, in particular termination.

In this paper, we show that step-indexing can in fact be used to prove termination of well-typed programs—even in the presence of dynamically-allocated, shared, mutable, higher-order state—so long as one’s type system enforces disciplined use of such state. Specifically, we consider a language with asynchronous channels, inspired by promises in JavaScript, in which higher-order state is used to implement communication, and linearity is used to ensure termination. The key to our approach is to generalize from natural number step-indexing to transfinite step-indexing, which enables us to compute termination bounds for program expressions in a compositional way. Although transfinite step-indexing has been proposed previously, we are the first to apply this technique to reasoning about termination in the presence of higher-order state.

References

[1]

Amal Ahmed, Andrew W Appel, Christopher D Richards, Kedar N Swadi, Gang Tan, and Daniel C Wang. 2010. Semantic foundations for typed assembly languages. ACM Transactions on Programming Languages and Systems (TOPLAS) 32, 3 ( 2010 ), 1-67. https://doi.org/10.1145/1709093.1709094

Digital Library

[2]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2005. A step-indexed model of substructural state. In Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming (Tallinn, Estonia) ( ICFP '05). Association for Computing Machinery, New York, NY, USA, 78-91. https://doi.org/10.1145/1086365.1086376

Digital Library

[3]

Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Ph.D. Dissertation. Princeton University.

Digital Library

[4]

Andrew W Appel and David McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 5 ( 2001 ), 657-683. https://doi.org/10.1145/ 504709.504712

Digital Library

[5]

Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. 2019. Simply RaTT: a Fitch-style modal calculus for reactive programming without space leaks. Proceedings of the ACM on Programming Languages 3, ICFP ( 2019 ), 1-27. https://doi.org/10.1145/3341713

Digital Library

[6]

Aleš Bizjak, Lars Birkedal, and Marino Miculan. 2014. A model of countable nondeterminism in guarded type theory. In Proceedings of TLCA. https://doi.org/10.1007/978-3-319-08918-8_8

[7]

Gérard Boudol. 2010. Typing termination in a higher-order concurrent imperative language. Information and Computation 208, 6 ( 2010 ), 716-736. https://doi.org/10.1016/j.ic. 2009. 06.007

Digital Library

[8]

Aloïs Brunel and Antoine Madet. 2012. Indexed realizability for bounded-time programming with references and type ifxpoints. In Asian Symposium on Programming Languages and Systems. Springer, 264-279. https://doi.org/10.1007/978-3-642-35182-2_19

[9]

Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pientka. 2014. Fair reactive programming. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, San Diego, California, USA, 361-372. https://doi.org/10.1145/2535838.2535881

Digital Library

[10]

Koen Claessen. 1999. A poor man's concurrency monad. Journal of Functional Programming 9, 3 ( 1999 ), 313-323. https: //doi.org/10.1017/S0956796899003342

Digital Library

[11]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular termination verification for non-blocking concurrency. In European Symposium on Programming. Springer, 176-201. https://doi.org/ 10.1007/978-3-662-49498-1_8

[12]

Robert Dockins and Aquinas Hobor. 2010. A theory of termination via indirection. In Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

[13]

Robert Dockins and Aquinas Hobor. 2012. Time bounds for general function pointers. Electronic Notes in Theoretical Computer Science 286 ( 2012 ), 139-155. https://doi.org/10.1016/j.entcs. 2012. 08.010

Digital Library

[14]

Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical step-indexed logical relations. Logical Methods in Computer Science 7, 2 : 16 ( 2011 ). https://doi.org/10.2168/LMCS-7( 2 :16) 2011

[15]

Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In POPL. 185-198. https://doi.org/10.1145/1706299.1706323

Digital Library

[16]

Daniel Friedman and David Wise. 1976. The impact of applicative programming on multiprocessing. In International Conference on Parallel Processing. 263-272.

[17]

Jean-Yves Girard. 1995. Light linear logic. In Logic and Computational Complexity, Daniel Leivant (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 145-176. https://doi.org/10.1007/3-540-60178-3_83

[18]

Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Cambridge University Press.

Digital Library

[19]

Gerhard Hessenberg. 1906. Grundbegrife der Mengenlehre. Vol. 1. Vandenhoeck & Ruprecht.

[20]

Alan Jefrey. 2012. LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012. Philadelphia, PA, USA, 49-60. https://doi.org/10.1145/2103776.2103783

Digital Library

[21]

Wolfgang Jeltsch. 2012. Towards a common categorical semantics for linear-time temporal logic and functional reactive programming. Electronic Notes in Theoretical Computer Science 286 ( 2012 ), 229-242. https://doi.org/10.1016/j.entcs. 2012. 08.015

Digital Library

[22]

Wolfgang Jeltsch. 2013. Temporal logic with "until", functional reactive programming with processes, and concrete process categories. In Proceedings of the 7th Workshop on Programming Languages Meets Program Verification (Rome, Italy) ( PLPV '13). ACM, New York, NY, USA, 69-78. https://doi.org/10.1145/2428116.2428128

Digital Library

[23]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. RustBelt: Securing the foundations of the Rust programming language. PACMPL 2, POPL, Article 66 ( 2018 ). https://doi.org/10.1145/3158154

Digital Library

[24]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 ( 2018 ). https://doi.org/10.1017/S0956796818000151

[25]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. ACM New York, NY, USA, 637-650. https://doi.org/10.1145/2676726.2676980

Digital Library

[26]

Neelakantan R. Krishnaswami. 2013. Higher-order functional reactive programming without spacetime leaks. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP '13). ACM, Boston, Massachusetts, USA, 221-232. https://doi.org/10.1145/2500365.2500588

Digital Library

[27]

Neelakantan R. Krishnaswami and Nick Benton. 2011. Ultrametric semantics of reactive programs. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. IEEE Computer Society, Washington, DC, USA, 257-266. https: //doi.org/10.1109/LICS. 2011.38

Digital Library

[28]

Neelakantan R Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. 2012. Superficially substructural types. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. 41-54. https://doi.org/10. 1145/2398856.2364536

Digital Library

[29]

Peter J Landin. 1964. The mechanical evaluation of expressions. Comput. J. 6, 4 ( 1964 ), 308-320. https://doi.org/10.1093/ comjnl/6.4. 308

[30]

Antoine Madet and Roberto M Amadio. 2011. An elementary afine-calculus with multithreading and side efects. In International Conference on Typed Lambda Calculi and Applications. Springer, 138-152. https://doi.org/10.1007/978-3-642-21691-6_13

[31]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019. Time credits and time receipts in Iris. In European Symposium on Programming. Springer, 3-29. https://doi.org/10.1007/978-3-030-17184-1_1

[32]

Greg Morrisett, Amal Ahmed, and Matthew Fluet. 2005. 3: A linear language with locations. In Typed Lambda Calculi and Applications, Paweł Urzyczyn (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 293-307. https://doi.org/10.1007/ 11417170_22

Digital Library

[33]

John C Reynolds. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress. 513-523.

[34]

Jan Schwinghammer, Aleš Bizjak, and Lars Birkedal. 2013. Step-indexed relational reasoning for countable nondeterminism. Logical Methods in Computer Science 9 ( 2013 ). https://doi.org/10.2168/LMCS-9( 4 :4) 2013

[35]

Simon Spies, Neel Krishnaswami, and Derek Dreyer. 2021. Transfinite step-indexing for termination. Technical Report. https://plv.mpi-sws.org/transfinite-step-indexing/termination/

[36]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In Proceedings of ESOP. https: //doi.org/10.1007/978-3-642-54833-8_9

Digital Library

[37]

Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. 2016. Transfinite step-indexing: Decoupling concrete and logical steps. In European Symposium on Programming. Springer, 727-751. https://doi.org/10.1007/978-3-662-49498-1_28

[38]

William W Tait. 1967. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32, 2 ( 1967 ), 198-212. https://doi.org/10.2307/2271658

[39]

Aaron J Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL. ACM New York, NY, USA, 343-356. https://doi.org/10.1145/2480359.2429111

Digital Library

[40]

Nobuko Yoshida, Martin Berger, and Kohei Honda. 2004. Strong normalisation in the-calculus. Information and Computation 191, 2 ( 2004 ), 145-202. https://doi.org/10.1016/j.ic. 2003. 08.004

Digital Library

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Goncharov SMilius STsampas SUrbat HSobocinski PLago UEsparza J(2024)Bialgebraic Reasoning on Higher-order Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662099(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662099
Spies SGäher LGratzer DTassarotti JKrebbers RDreyer DBirkedal LFreund SYahav E(2021)Transfinite Iris: resolving an existential dilemma of step-indexed separation logicProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454031(80-95)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454031
Show More Cited By

Index Terms

Transfinite step-indexing for termination
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Step-indexed separation logic has proven to be a powerful tool for modular reasoning about higher-order stateful programs. However, it has only been used to reason about safety properties, never liveness properties. In this paper, we observe that the ...
Cyclic proofs of program termination in separation logic
POPL '08

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when ...
Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Horizon 2020 Framework Programme

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
638
Total Downloads

Downloads (Last 12 months)110
Downloads (Last 6 weeks)22

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Goncharov SMilius STsampas SUrbat HSobocinski PLago UEsparza J(2024)Bialgebraic Reasoning on Higher-order Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662099(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662099
Spies SGäher LGratzer DTassarotti JKrebbers RDreyer DBirkedal LFreund SYahav E(2021)Transfinite Iris: resolving an existential dilemma of step-indexed separation logicProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454031(80-95)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454031
Jaber GRiba C(2021)Temporal Refinements for Guarded Recursive TypesProgramming Languages and Systems10.1007/978-3-030-72019-3_20(548-578)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_20

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents