Execution time of λ-terms via denotational semantics and intersection types

被引：39
|
作者：
De Carvalho, Daniel [1 ]
机构：
[1] Innopolis Univ, Univ Skaya St 1, Innopolis 420500, Tatarstan, Russia
来源：
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2018年 / 28卷 / 07期
关键词：
CALCULUS;
D O I：
10.1017/S0960129516000396
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The multiset-based relational model of linear logic induces a semantics of the untyped lambda-calculus, which corresponds with a non-idempotent intersection type system, System R. We prove that, in System R, the size of type derivations and the size of types are closely related to the execution time of lambda-terms in a particular environment machine, Krivine's machine.
引用
收藏
页码：1169 / 1203
页数：35
相关论文
共 50 条
  • [1] Denotational Semantics for Symbolic Execution
    Voogd, Erik
    Klovstad, Asmund Aqissiaq Arild
    Johnsen, Einar Broch
    THEORETICAL ASPECTS OF COMPUTING, ICTAC 2023, 2023, 14446 : 370 - 387
  • [2] Denotational Cost Semantics for Functional Languages with Inductive Types
    Danner, Norman
    Licata, Daniel R.
    Ramyaa, Ramyaa
    PROCEEDINGS OF THE 20TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING (ICFP'15), 2015, : 140 - 151
  • [3] Denotational Cost Semantics for Functional Languages with Inductive Types
    Danner, Norman
    Licata, Daniel R.
    Ramyaa, Ramyaa
    ACM SIGPLAN NOTICES, 2015, 50 (09) : 140 - 151
  • [4] Characterizing convergent terms in object calculi via intersection types
    de'Liguoro, U
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2001, 2044 : 315 - 328
  • [5] Denotational linear time semantics and sequential composition
    Baier, C
    MajsterCederbaum, ME
    INFORMATION PROCESSING LETTERS, 1996, 59 (03) : 135 - 143
  • [6] Denotational semantics of recursive types in synthetic guarded domain theory
    Mogelberg, Rasmus E.
    Paviotti, Marco
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2019, 29 (03) : 465 - 510
  • [7] Denotational semantics of recursive types in synthetic guarded domain theory
    Mogelberg, Rasmus Ejlers
    Paviotti, Marco
    PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 317 - 326
  • [8] Towards Univalent Reference Types The Impact of Univalence on Denotational Semantics
    Sterling, Jonathan
    Gratzer, Daniel
    Birkedal, Lars
    32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
  • [9] Denotational semantics for synchronous and asynchronous behavior with multiform time
    Roncken, M.
    Gerth, R.
    Proceedings of the International BCS-FACS Workshop, 1990,
  • [10] Semantics for Combinatory Logic With Intersection Types
    Ghilezan, Silvia
    Kasterovic, Simona
    FRONTIERS IN COMPUTER SCIENCE, 2022, 4
12345