More Web Proxy on the site http://driver.im/

Article

A bisimulation for type abstraction and recursion

Authors:

Benjamin C. PierceAuthors Info & Claims

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 63 - 74

https://doi.org/10.1145/1040305.1040311

Published: 12 January 2005 Publication History

Abstract

We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and ΤΤ-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider sets of relations---instead of just relations---as bisimulations.

References

[1]

M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 104--115, 2001.

Digital Library

[2]

M. Abadi and A. D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5:267--303, 1998. Preliminary version appeared inph7th European Symposium on Programming,phLecture Notes in Computer Science, Springer-Verlag, vol. 1381, pp. 12--26, 1998.

Digital Library

[3]

M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1--70, 1999. Preliminary version appeared inphProceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36--47, 1997.

Digital Library

[4]

S. Abramsky. The lazy lambda calculus. In D. A. Turner, editor, Research Topics in Functional Programming, pages 65--117. Addison-Wesley, 1990.

Digital Library

[5]

A. Ahmed, A. W. Appel, and R. Virga. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~amal/papers/impred.pdf, 2003.

[6]

A. W. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657--683, 2001.

Digital Library

[7]

M. Berger, K. Honda, and N. Yoshida. Genericity and the pi-calculus. In Foundations of Software Science and Computation Structures, volume 2620 of Lecture Notes in Computer Science, pages 103--119. Springer-Verlag, 2003.

Digital Library

[8]

G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Higher Order Operational Techniques in Semantics, volume~41 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2000.

[9]

L. Birkedal and R. Harper. Relational interpretations of recursive types in an operational setting. Information and Computation, 155(1--2):3--63, 1999. Summary appeared inphTheoretical Aspects of Computer Software,phLecture Notes in Computer Science, Springer-Verlag, vol. 1281, pp. 458--490, 1997.

Digital Library

[10]

M. Boreale, R. De Nicola, and R. Pugliese. Proof techniques for cryptographic processes. SIAM Journal on Computing, 31(3):947--986, 2002. Preliminary version appeared inph14th Annual IEEE Symposium on Logic in Computer Science, pp. 157--166, 1999.

Digital Library

[11]

J. Borgström and U. Nestmann. On bisimulations for the spi calculus. In 9th International Conference on Algebraic Methodology and Software Technology, volume 2422 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2002.

Digital Library

[12]

K. B. Bruce, L. Cardelli, and B. C. Pierce. Comparing object encodings. Information and Computation, 155(1--2):108--133, 1999. Extended abstract appeared inphTheoretical Aspects of Computer Software, Springer-Verlag, vol. 1281, pp. 415--338, 1997.

Digital Library

[13]

K. Crary and R. Harper. Syntactic logical relations over polymorphic and recursive types. Draft, 2000.

[14]

A. D. Gordon. Bisimilarity as a theory of functional programming. mini-course. http://research.microsoft.com/~adg/Publications/BRICS-NS-95-3.dvi.gz, 1995.

[15]

A. D. Gordon. Operational equivalences for untyped and polymorphic object calculi. In Higher Order Operational Techniques in Semantics, pages 9--54, 1995.

Digital Library

[16]

A. D. Gordon and G. D. Rees. Bisimilarity for F‹:. Draft, 1995.

[17]

A. D. Gordon and G. D. Rees. Bisimilarity for a first-order calculus of objects with subtyping. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 386--395, 1996.

Digital Library

[18]

N. Heintze and J. G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998.

Digital Library

[19]

D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103--112, 1996.

Digital Library

[20]

D. J. Hughes. Games and definability for System F. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 76--86, 1997.

Digital Library

[21]

R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980.

Digital Library

[22]

R. Milner. Communication and Concurrency. Springer-Verlag, 1995.

Digital Library

[23]

R. Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999.

Digital Library

[24]

J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.

Digital Library

[25]

E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55--92, 1991.

Digital Library

[26]

J. H. Morris, Jr. Protection in programming languages. Communications of the ACM, 16(1):15--21, 1973.

Digital Library

[27]

J. H. Morris, Jr. Types are not sets. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 120--124, 1973.

Digital Library

[28]

B. C. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM, 47(3):531--586, 2000. Extended abstract appeared inphProceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 531--584.

Digital Library

[29]

A. M. Pitts. Existential types: Logical relations and operational equivalence. In Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 309--326. Springer-Verlag, 1998.

Digital Library

[30]

A. M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321--359, 2000. Preliminary version appeared inphHOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics,phElectronic Notes in Theoretical Computer Science, vol. 10, 1998.

Digital Library

[31]

A. M. Pitts and I. Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, pages 227--273. Cambridge University Press, 1998.

Digital Library

[32]

D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigm. PhD thesis, University of Edinburgh, 1992.

[33]

D. Sangiorgi and R. Milner. The problem of "weak bisimulation up to". In CONCUR '92, Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 32--46. Springer-Verlag, 1992.

Digital Library

[34]

E. Sumii and B. C. Pierce. A bisimulation for dynamic sealing. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 161--172, 2004.

Digital Library

[35]

E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. Technical Report MS-CIS-04-27, Department of Computer and Information Science, University of Pennsylvania, 2004. http://www.cis.upenn.edu/~sumii/pub/.

[36]

P. Wadler. Theorems for free! In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 347--359. ACM, 1989.

Digital Library

Cited By

Clune JRamamurthy VMartins RAcar U(2020)Program equivalence for assisted grading of functional programsProceedings of the ACM on Programming Languages10.1145/34282394:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428239
Samak MKim DRinard M(2019)Synthesizing replacement classesProceedings of the ACM on Programming Languages10.1145/33711204:POPL(1-33)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371120
Pous DSangiorgi D(2019)Bisimulation and Coinduction Enhancements: A Historical PerspectiveFormal Aspects of Computing10.1007/s00165-019-00497-wOnline publication date: 8-Nov-2019
https://doi.org/10.1007/s00165-019-00497-w
Show More Cited By

Index Terms

A bisimulation for type abstraction and recursion
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

A bisimulation for type abstraction and recursion

We present a bisimulation method for proving the contextual equivalence of packages in λ-calculus with full existential and recursive types. Unlike traditional logical relations (either semantic or syntactic), our development is “elementary,” using only ...
A bisimulation for type abstraction and recursion
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development ...
Small bisimulations for reasoning about higher-order imperative programs
Proceedings of the 2006 POPL Conference

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
572
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Clune JRamamurthy VMartins RAcar U(2020)Program equivalence for assisted grading of functional programsProceedings of the ACM on Programming Languages10.1145/34282394:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428239
Samak MKim DRinard M(2019)Synthesizing replacement classesProceedings of the ACM on Programming Languages10.1145/33711204:POPL(1-33)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371120
Pous DSangiorgi D(2019)Bisimulation and Coinduction Enhancements: A Historical PerspectiveFormal Aspects of Computing10.1007/s00165-019-00497-wOnline publication date: 8-Nov-2019
https://doi.org/10.1007/s00165-019-00497-w
Wang YDillig ILahiri SCook W(2017)Verifying equivalence of database-driven applicationsProceedings of the ACM on Programming Languages10.1145/31581442:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158144
Schmidt-Schauíß MSabel DNiehren JSchwinghammer J(2015)Observational program calculi and the correctness of translationsTheoretical Computer Science10.1016/j.tcs.2015.02.027577:C(98-124)Online publication date: 27-Apr-2015
https://dl.acm.org/doi/10.1016/j.tcs.2015.02.027
Benton NHofmann MNigam V(2014)Abstract effects and proof-relevant logical relationsACM SIGPLAN Notices10.1145/2578855.253586949:1(619-631)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535869
Benton NHofmann MNigam VJagannathan SSewell P(2014)Abstract effects and proof-relevant logical relationsProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535869(619-631)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535869
Sangiorgi D(2014)Higher-Order Languages: Bisimulation and Coinductive Equivalences (Extended Abstract)Advanced Information Systems Engineering10.1007/978-3-662-44124-4_1(3-9)Online publication date: 20-Aug-2014
https://doi.org/10.1007/978-3-662-44124-4_1
Sangiorgi D(2013)Coinductive techniques for higher-order languagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.131.1131(1-4)Online publication date: 15-Oct-2013
https://doi.org/10.4204/EPTCS.131.1
Fournet CSwamy NChen JDagand PStrub PLivshits B(2013)Fully abstract compilation to JavaScriptACM SIGPLAN Notices10.1145/2480359.242911448:1(371-384)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429114
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.

Media

Figures

Other

Tables

View Table of Contents