A simple take on typed abstract syntax in Haskell-like languages

被引：0
|
作者：
Danvy, O [1 ]
Rhiger, M [1 ]
机构：
[1] Aarhus Univ, Dept Comp Sci, DK-8000 Aarhus C, Denmark
来源：
FUNCTIONAL AND LOGIC PROGRAMMING, PROCEEDINGS | 2001年 / 2024卷
关键词：
type-directed partial evaluation; normalization functions; simply typed lambda-calculus; higher-order abstract syntax; Haskell;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a simple way to program typed abstract syntax in a language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions. as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.
引用
收藏
页码：343 / 358
页数：16
相关论文
共 21 条
  • [1] A family of syntactic logical relations for the semantics of Haskell-like languages
    Johann, Patricia
    Voigtlaender, Janis
    [J]. INFORMATION AND COMPUTATION, 2009, 207 (02) : 341 - 368
  • [2] Normalization by evaluation with typed abstract syntax
    Danvy, O
    Rhiger, M
    Rose, KH
    [J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2001, 11 : 673 - 680
  • [3] EXTENDED INITIALITY FOR TYPED ABSTRACT SYNTAX
    Ahrens, Benedikt
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (02)
  • [4] Abstract syntax and semantics of visual languages
    Erwig, M
    [J]. JOURNAL OF VISUAL LANGUAGES AND COMPUTING, 1998, 9 (05): : 461 - 483
  • [5] Implementing a Category-Theoretic Framework for Typed Abstract Syntax
    Ahrens, Benedikt
    Matthes, Ralph
    Mortberg, Anders
    [J]. PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 307 - 323
  • [6] A Generic Abstract Syntax Model for Embedded Languages
    Axelsson, Emil
    [J]. ACM SIGPLAN NOTICES, 2012, 47 (09) : 323 - 334
  • [7] Generator of efficient strongly typed abstract syntax trees in Java']Java
    van den Brand, M
    Moreau, PE
    Vinju, J
    [J]. IEE PROCEEDINGS-SOFTWARE, 2005, 152 (02): : 70 - 78
  • [8] Bridging concrete and abstract syntax of Web rule languages
    Milanovic, Milan
    Gasevic, Dragan
    Giurca, Adrian
    Wagner, Gerd
    Lukichev, Sergey
    Devedzic, Vladan
    [J]. WEB REASONING AND RULE SYSTEMS, PROCEEDINGS, 2007, 4524 : 309 - +
  • [9] Integrated definition of abstract and concrete syntax for textual languages
    Krahn, Holger
    Rumpe, Bernhard
    Voelkel, Steven
    [J]. MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2007, 4735 : 286 - +
  • [10] A simple approach to supporting untagged objects in dynamically typed languages
    Bigot, PA
    Debray, SK
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1997, 32 (01): : 25 - 47
123