A Type Theoretic Specification of Partial Evaluation

被引：1
|
作者：
Asai, Kenichi [1 ]
Fennell, Luminous [2 ]
Thiemann, Peter [2 ]
Zhang, Yang [2 ]
机构：
[1] Ochanomizu Univ, Tokyo, Japan
[2] Univ Freiburg, Freiburg, Germany
来源：
PPDP'14: PROCEEDINGS OF THE 16TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING | 2014年
关键词：
partial evaluation; dependently-typed programming; typed metaprogramming;
D O I：
10.1145/2643135.2643146
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We develop a type theoretic specification of offline partial evaluation for the simply-typed lambda calculus in the dependently-typed programming language Agda. We establish the correctness of the specification by proving termination, typing preservation, and semantics preservation using logical relations. Typing preservation is achieved by relying on a typed syntax representation based on De Bruijn indices for the source and the target language. The full calculus contains primitive recursion on natural numbers and higherorder lifting for function, product, and sum types.
引用
收藏
页码：57 / 68
页数：12
相关论文
共 50 条
  • [1] TECHNIQUES FOR PARTIAL SPECIFICATION AND SPECIFICATION OF SWITCHING SYSTEMS
    ZAVE, P
    JACKSON, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 551 : 511 - 525
  • [2] PARTIAL HYPERBOLICITY AND SPECIFICATION
    Sumi, Naoya
    Varandas, Paulo
    Yamamoto, Kenichiro
    [J]. PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 2016, 144 (03) : 1161 - 1170
  • [3] Type-directed partial evaluation
    Danvy, O
    [J]. PARTIAL EVALUATION: PRACTICE AND THEORY, 1999, 1706 : 367 - 411
  • [4] Specification and partial hyperbolicity for flows
    Sumi, Naoya
    Varandas, Paulo
    Yamamoto, Kenichiro
    [J]. DYNAMICAL SYSTEMS-AN INTERNATIONAL JOURNAL, 2015, 30 (04): : 501 - 524
  • [5] Memoization in type-directed partial evaluation
    Balat, V
    Danvy, O
    [J]. GENERATIVE PROGRAMMING AND COMPONENT ENGINEERING 2002, PROCEEDINGS, 2002, 2487 : 78 - 92
  • [6] TYPE INFERENCE BY PROGRAM TRANSFORMATION AND PARTIAL EVALUATION
    FRUHWIRTH, TW
    [J]. META-PROGRAMMING IN LOGIC PROGRAMMING, 1989, : 263 - 282
  • [7] Evaluation of absolute type in the Partial Goals Method
    Jandova, Vera
    Talasova, Jana
    [J]. 33RD INTERNATIONAL CONFERENCE MATHEMATICAL METHODS IN ECONOMICS (MME 2015), 2015, : 321 - 326
  • [8] Towards a proof-theoretic foundation for actor specification and verification
    Duarte, CHC
    [J]. FORMAL MODELS OF AGENTS, 1999, 1760 : 123 - 142
  • [9] RELIGIOUS INSTITUTIONS IN COMPLEX SOCIETIES - DIFFICULTIES IN THE THEORETIC SPECIFICATION OF FUNCTIONS
    EISTER, AW
    [J]. AMERICAN SOCIOLOGICAL REVIEW, 1957, 22 (04) : 387 - 391
  • [10] SEPARATE COMPILATION AND PARTIAL SPECIFICATION IN PASCAL
    CELENTANO, A
    DELLAVIGNA, P
    GHEZZI, C
    MANDRIOLI, D
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1980, 6 (04) : 320 - 328
12345