Dependent Type Inference with Interpolants

被引：44
|
作者：
Unno, Hiroshi [1 ]
Kobayashi, Naoki [1 ]
机构：
[1] Tohoku Univ, Sendai, Miyagi 980, Japan
来源：
PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING | 2009年
关键词：
Dependent Types; Type Inference;
D O I：
10.1145/1599410.1599445
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We propose a novel type inference algorithm for a dependently-typed functional language. The novel features of our algorithm are: (i) it can iteratively refine dependent types with interpolants until the type inference succeeds or the program is found to be ill-typed, and (ii) in the latter case, it can generate a kind of counter-example as an explanation of why the program is ill-typed. We have implemented a prototype type inference system and tested it for several programs.
引用
收藏
页码：277 / 288
页数：12
相关论文
共 50 条
  • [1] TYPE-DEPENDENT PARAMETER INFERENCE
    CORMACK, GV
    WRIGHT, AK
    SIGPLAN NOTICES, 1990, 25 (06): : 127 - 136
  • [2] Taylor type and Hermite type interpolants in Rn
    Van Manh, Phung
    Van Trao, Nguyen
    Tung, Phan Thanh
    Cuong, Le Ngoc
    NUMERICAL ALGORITHMS, 2022, 89 (01) : 145 - 166
  • [3] Dependent Array Type Inference from Tests
    Zhu, He
    Nori, Aditya V.
    Jagannathan, Suresh
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2015), 2015, 8931 : 412 - 430
  • [4] Compositional and Lightweight Dependent Type Inference for ML
    Zhu, He
    Jagannathan, Suresh
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2013), 2013, 7737 : 295 - 314
  • [5] Interpolation on the hypersphere with Thiele type rational interpolants
    Gensane, Thierry
    NUMERICAL ALGORITHMS, 2012, 60 (03) : 523 - 529
  • [6] ON SIMULTANEOUS RATIONAL INTERPOLANTS OF TYPE (ALPHA,BETA)
    PIEDRA, R
    LECTURE NOTES IN MATHEMATICS, 1988, 1354 : 188 - 198
  • [7] Interpolation on the hypersphere with Thiele type rational interpolants
    Thierry Gensane
    Numerical Algorithms, 2012, 60 : 523 - 529
  • [8] SHAPE-DEPENDENT MOTION INTERPOLANTS FOR PLANAR OBJECTS
    Liu, Huan
    Ge, Qiaode Jeffrey
    Langer, Mark P.
    PROCEEDINGS OF ASME 2023 INTERNATIONAL DESIGN ENGINEERING TECHNICAL CONFERENCES AND COMPUTERS AND INFORMATION IN ENGINEERING CONFERENCE, IDETC-CIE2023, VOL 8, 2023,
  • [9] Bivariate interpolation on the hypersphere with thiele type rational interpolants
    Tang, Shuo, 1600, Binary Information Press (11):
  • [10] On Chebyshev-type discrete quasi-interpolants
    Jose Ibanez-Perez, Maria
    MATHEMATICS AND COMPUTERS IN SIMULATION, 2008, 77 (2-3) : 218 - 227
12345