research-article

Linear lambda calculus with non-linear first-class continuations

Author:

Shin-Ya NishizakiAuthors Info & Claims

ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

Pages 28 - 32

https://doi.org/10.1145/3056662.3056693

Published: 26 February 2017 Publication History

Abstract

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional languages with respect to logical negation. My previous paper and other researchers' studies reveal that we can obtain a first-class continuation mechanism by providing duplicability and removability of continuations, which is equivalent to the right-contraction and weakening rules in Gentzen's deductive system, the sequent calculus. In the lambda calculus, it is allowed to duplicate and remove values, but the continuations are impossible to duplicate and remove. In our previous paper, we showed that we can obtain the lambda calculus with first-class continuations providing duplicability and removability of both values and continuations. In this paper, we will study a calculus in which we only have duplicability and removability of continuations. We formalize this calculus in the framework of linear logic, which is a logical system sensitive to duplicability and removability, proposed by Jean-Yves Girard.

References

[1]

A. Bhery, S. Hagihara, and N. Yonezaki. A formal system for analysis of cryptographic encryption and their security properties. 3233:87--112, 2004.

[2]

A. Filinski. Declarative continuations and categorical duality, 1989.

[3]

J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1--101, 1987.

Digital Library

[4]

J.-Y. Girard and Y. Lafont. Proof and types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[5]

J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types, volume 7 of Cambridge Tracts in Computer Science. Cambridge University Press, 1989.

[6]

R. Ikeda, K. Narita, and S. ya Nishizaki. Cooperation of model checking and network simulation for cost analyses of distributed systems. International Journal of Computers and Applications, 33(4):323--329, 2011.

[7]

S. Ito, T. Ichinose, M. Shimakawa, N. Izumi, S. Hagihara, and N. Yonezaki. Modular analysis of gene networks by linear temporal logic. Journal of Integrative Bioinformatics, 10(2):216.

[8]

S. Ito, T. Ichinose, M. Shimakawa, N. Izumi, S. Hagihara, and N. Yonezaki. Qualitative analysis of gene regulatory networks by temporal logic. Theoretical Computer Science, 594(23):151--179, August 2015.

Digital Library

[9]

E. Kuma, S. Nishizaki, and T. Watanabe. Modifiable continuation in object calculus. In Theory and Practice of Computtion, volume 5 of Proceedings of Information and Communications Technology, pages 160--173. Springer Japan, 2012.

[10]

Y. Lafont. The linear abstract machine. Theoretical computer science, 59(1--2):157--180, 1988.

[11]

S. Matsumoto and S. Nishizaki. An object calculus with remote method invocation. In Theory and Practice of Computation, volume 7 of Proceedings in Information and Communications Technology, pages 34--49. Springer Japan.

[12]

C. Murthy. An evaluation semantics for classical proofs. In Proc. 5th IEEE Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[13]

K. Narita and S. Nishizaki. A Parallel Abstract Machine for the RPC Calculus. In Proceedings of the International Science - ICIEIS 2011, volume 253 of Communications in Computer and Information Science, pages 320--332. Springer, 2011.

[14]

S. Nishizaki. Programs with continuations and linear logic. Science of Computer Programming, 21(2):95--116, 1994.

Digital Library

[15]

S. Nishizaki. Polymorphic environment calculus and its type inference algorithm. Higher-Order and Symbolic Computation, 13(3), 2000.

Digital Library

[16]

S. Nishizaki. Evaluation strategy and translation of environment calculus. In Information Computing and Applications, volume 391 of Communications in Computer and Information Science, pages 232--242. Springer, 2013.

[17]

S. Nishizaki, M. Fujii, and R. Ikeda. Process Calculus for Cost Analysis of Process Creation. In Proceedings of the 2012 International Conference on Information Technology and Software Engineering, Lecture Notes in Electrical Engineering, pages 33--40. Springer-Verlag Berlin Heidelberg, 2013.

[18]

T. Ohata and S. Nishizaki. Let-binding with regular expressions in lambda calculus. Journal of Software, 11(2):220--229, 2016.

[19]

M. Shimakawa, S. Hagihara, and N. Yonezaki. Complexity of strong satisfiability problems for reactive system specifications. IEICE Transactions on Information and Systems, E96.D(10):2187--2193, 2013.

[20]

D. Tomioka, S. Nishizaki, and R. Ikeda. A cost estimation calculus for analyzing the resistance to denial-of-service attack. In Software Security - Theories and Systems, volume 3233 of Lecture Notes in Computer Science, pages 25--44. Springer Berlin, 2004.

[21]

P. Wadler. Call-by-Value Is Dual to Call-by-Name --- Reloaded. Volume 3467 of Lecture Notes in Computer Science, pages 185--203. Springer Berlin Heidelberg, 2005.

Cited By

Nishizaki S(2019)ML Polymorphism of Linear Lambda Calculus with First-class ContinuationsProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316668(189-193)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316668
Shin-Ya N(2017)Type Inference of Linear Lambda Calculus with First-Class Continuations2017 International Conference on Computer Technology, Electronics and Communication (ICCTEC)10.1109/ICCTEC.2017.00040(149-152)Online publication date: Dec-2017
https://doi.org/10.1109/ICCTEC.2017.00040

Index Terms

Linear lambda calculus with non-linear first-class continuations
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Functional constructs

Recommendations

ML Polymorphism of Linear Lambda Calculus with First-class Continuations
ICSCA '19: Proceedings of the 2019 8th International Conference on Software and Computer Applications

The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system; propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to an evaluation strategy. Furthermore, ...
Infinitary Lambda Calculi from a Linear Perspective
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

We introduce a linear infinitary λ-calculus, called ℓΛ∞, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the ...
Focused Linear Logic and the λ-calculus

Linear logic enjoys strong symmetries inherited from classical logic while providing a constructive framework comparable to intuitionistic logic. However, the computational interpretation of sequent calculus presentations of linear logic remains ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

February 2017

339 pages

ISBN:9781450348577

DOI:10.1145/3056662

Conference Chairs:
Vitaliy Mezhuyev
Universiti Malaysia Pahang, Malaysia
,
Luigi Benedicenti
University of Regina, Canada

Copyright © 2017 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: 26 February 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSCA 2017

ICSCA 2017: 2017 6th International Conference on Software and Computer Applications

February 26 - 28, 2017

Bangkok, Thailand

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
61
Total Downloads

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

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nishizaki S(2019)ML Polymorphism of Linear Lambda Calculus with First-class ContinuationsProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316668(189-193)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316668
Shin-Ya N(2017)Type Inference of Linear Lambda Calculus with First-Class Continuations2017 International Conference on Computer Technology, Electronics and Communication (ICCTEC)10.1109/ICCTEC.2017.00040(149-152)Online publication date: Dec-2017
https://doi.org/10.1109/ICCTEC.2017.00040

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