Foundations of Symmetric λ-calculus

• SAKAUE Sari

  Ochanomizu University

• ASAI Kenichi

  Ochanomizu University

Bibliographic Information

Other Title

• 対称λ計算の基礎理論
• タイショウ ラムダ ケイサン ノ キソ リロン

Abstract

Continuations represent “the rest of the computation.” We use control operators in order to manipulate continuations and represent non-local transfer of control. However, it is not easy to represent such a complex control structure in a programming language. To manipulate continuations in a uniform way, this paper presents a calculus, called a symmetric λ-calculus (SLC). It is based on the calculus presented by Filinski, and deals with terms and continuations in a systematic and symmetric way. We formulate this system by small step semantics, and prove that SLC satisfies the basic properties of typed languages, namely progress and preservation. Then, we show the following two transformations: (1) from Felleisen's Λ_C-calculus with the control operator C to the call-by-value SLC, and (2) from Parigot's call-by-name λμ-calculus to the call-by-name SLC. These transformations show that SLC is suitable as a base calculus for discussing various aspects of continuations. We expect to relate this symmetry between call-by-value and call-by-name to the symmetry between terms and continuations.

Journal

• Computer Software

  Computer Software 26 (2), 3-17, 2009

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713179136
• NII Article ID: 10025982342
• NII Book ID: AN10075819
• DOI: 10.11309/jssst.26.2_3
• NDL BIB ID: 10290018
• ISSN: 02896540
• Web Site: http://id.ndl.go.jp/bib/10290018
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I10290018
• Data Source:
  • JaLC
  • NDL
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed