HASCASL: Integrated higher-order specification and program development

被引：14
|
作者：
Schroeder, Lutz [1 ]
Mossakowski, Till
机构：
[1] Univ Bremen, DFKI Lab Breman, D-2800 Bremen 33, Germany
来源：
THEORETICAL COMPUTER SCIENCE | 2009年 / 410卷 / 12-13期
关键词：
Algebraic specification; Functional programming; Type classes; Polymorphism; CASL; Monads; Hoare logic; Higher-order logic; ALGEBRAIC SPECIFICATIONS; DYNAMIC LOGIC; SET;
D O I：
10.1016/j.tcs.2008.11.020
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We lay out the design of HASCASL, a higher order extension of the algebraic specification language CASL that serves both as a wide-spectrum language for the rigorous specification and development of software, in particular but not exclusively in modern functional programming languages, and as an expressive standard language for higher-order logic. Distinctive features of HASCASL include partial higher order functions, higher order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HASCASL provides dedicated specification support for monad-based functional-imperative programming with generic side effects, including a monad-based generic Hoare logic. (C) 2008 Elsevier B.V. All rights reserved.
引用
收藏
页码：1217 / 1260
页数：44
相关论文
共 50 条
  • [41] SPECIFICATION AND VERIFICATION OF DIGITAL SYSTEMS USING HIGHER-ORDER PREDICATE LOGIC.
    Hanna, F.K.
    Daeche, N.
    [J]. 1600, (133):
  • [42] An observationally complete program logic for imperative higher-order functions
    Honda, Kohei
    Yoshida, Nobuko
    Berger, Martin
    [J]. THEORETICAL COMPUTER SCIENCE, 2014, 517 : 75 - 101
  • [43] An observationally complete program logic for imperative higher-order functions
    Honda, K
    Yoshida, N
    Berger, M
    [J]. LICS 2005: 20th Annual IEEE Symposium on Logic in Computer Science - Proceedings, 2005, : 270 - 279
  • [44] Higher-order mode substrate integrated rectangular patch antenna
    Kumar, Jayendra
    [J]. AEU-INTERNATIONAL JOURNAL OF ELECTRONICS AND COMMUNICATIONS, 2021, 139
  • [45] Substrate Integrated Waveguide Filter with Higher-Order Modes Suppression
    Ma, Liang
    Li, Jiang
    Zhou, Yongchun
    Sun, Xun
    Zhu, Honghao
    [J]. 2018 INTERNATIONAL CONFERENCE ON MICROWAVE AND MILLIMETER WAVE TECHNOLOGY (ICMMT2018), 2018,
  • [46] Higher-Order Program Verification and Language-Based Security
    Kobayashi, Naoki
    [J]. ADVANCES IN COMPUTER SCIENCE - ASIAN 2009: INFORMATION SECURITY AND PRIVACY, PROCEEDINGS, 2009, 5913 : 17 - 23
  • [47] Program logic for higher-order probabilistic programs in Isabelle/HOL
    Hirata, Michikazu
    Minamide, Yasuhiko
    Sato, Tetsuya
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2023, 230
  • [48] LAMBDABEAM: Neural Program Search with Higher-Order Functions and Lambdas
    Shi, Kensen
    Dai, Hanjun
    Li, Wen-Ding
    Ellis, Kevin
    Sutton, Charles
    [J]. ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 36 (NEURIPS 2023), 2023,
  • [49] A SIMPLE ESTIMATOR OF COINTEGRATING VECTORS IN HIGHER-ORDER INTEGRATED SYSTEMS
    STOCK, JH
    WATSON, MW
    [J]. ECONOMETRICA, 1993, 61 (04) : 783 - 820
  • [50] Higher-order improvements of the sieve bootstrap for fractionally integrated processes
    Poskitt, D. S.
    Grose, Simone D.
    Martin, Gael M.
    [J]. JOURNAL OF ECONOMETRICS, 2015, 188 (01) : 94 - 110
12345