Hostname: page-component-669899f699-cf6xr Total loading time: 0 Render date: 2025-04-26T04:00:10.463Z Has data issue: false hasContentIssue false
  • English
  • Français

Control effects as a modality

Published online by Cambridge University Press:  01 January 2009

HAYO THIELECKE
HAYO THIELECKE*
Affiliation:
University of Birmingham, Birmingham, UK (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.

Type
Theoretical Pearls
Information
Journal of Functional Programming , Volume 19 , Issue 1 , January 2009 , pp. 17 - 26
Copyright
Copyright © Cambridge University Press 2008

References

Benton, P. N., Bierman, G. M., & de Paiva, V. (1998) Computational types from a logical perspective. J. Functional Programming 8 (2), 177–193.CrossRefGoogle Scholar
Felleisen, M. (1991) On the expressive power of programming languages. Sci. Comput. Program, 17 (1–3), 35–75.CrossRefGoogle Scholar
Felleisen, M., & Hieb, R. (1992) The revised report on the syntactic theories of sequential control and state. Theor. Comp. Sci. 103 (2), 235–271.CrossRefGoogle Scholar
Griffin, T. G. (1990) A formulae-as-types notion of control. In Principles of Programming Languages (POPL). ACM, New York, NY, USA, pp. 47–58.Google Scholar
Jouvelot, P., & Gifford, D. K. (1988) Reasoning about continuations with control effects. In Programming Language Design and Implementation (PLDI). ACM, New York, NY, USA, pp. 218–226.Google Scholar
Lucassen, J. M., & Gifford, D. K. (1988) Polymorphic effect systems. In Principles of Programming Languages (POPL). ACM, New York, NY, USA, pp. 47–57.Google Scholar
Moggi, E. (1989) Computational lambda calculus and monads. In Logic in Computer Science (LICS). IEEE, Pacific Grove, CA, USA, pp. 14–23.Google Scholar
Thielecke, H. (2003) From control effects to typed continuation passing. In Principles of Programming Languages (POPL). ACM, New York, NY, USA, pp. 139–149.Google Scholar
Thielecke, H. (2004) Answer type polymorphism in call-by-name continuation passing. In European Symposium on Programming (ESOP). LNCS, vol. 2986. Springer, Berlin/Heidelberg, pp. 279–293.Google Scholar
Troelstra, A. S., & Schwichtenberg, H. (2000) Basic Proof Theory. Cambridge University Press, New York, NY, USA.CrossRefGoogle Scholar
Wadler, P. (1998) The marriage of effects and monads. In International Conference on Functional Programming (ICFP). ACM, New York, NY, USA, pp. 63–74.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.