Datatype-Generic Termination Proofs

被引：1
|
作者：
Backhouse, Roland [1 ]
Doornbos, Henk [2 ]
机构：
[1] Univ Nottingham, Sch Comp Sci & Informat Technol, Nottingham NG8 1BB, England
[2] Questance, NL-9711 TS Groningen, Netherlands
来源：
THEORY OF COMPUTING SYSTEMS | 2008年 / 43卷 / 3-4期
基金：
英国工程与自然科学研究理事会;
关键词：
Datatype; Generic programming; Relation algebra; Allegory; Programming methodology;
D O I：
10.1007/s00224-007-9056-z
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Datatype-generic programs are programs that are parameterised by a datatype. We review the allegorical foundations of a methodology of designing datatype-generic programs. The notion of F-reductivity, where F parametrises a datatype, is reviewed and a number of its properties are presented. The properties are used to give concise, effective proofs of termination of a number of datatype-generic programming schemas. The paper concludes with a concise proof of the well-foundedness of a datatype-generic occurs-in relation.
引用
收藏
页码：362 / 393
页数：32
相关论文
共 50 条
  • [1] Datatype-Generic Termination Proofs
    Roland Backhouse
    Henk Doornbos
    [J]. Theory of Computing Systems, 2008, 43 : 362 - 393
  • [2] Datatype-generic reasoning
    Backhouse, Roland
    [J]. LOGICAL APPROACHES TO COMPUTATIONAL BARRIERS, PROCEEDINGS, 2006, 3988 : 21 - 34
  • [3] Datatype-generic programming
    Gibbons, Jeremy
    [J]. DATATYPE-GENERIC PROGRAMMING, 2007, 4719 : 1 - +
  • [4] Arity-Generic Datatype-Generic Programming
    Weirich, Stephanie
    Casinghino, Chris
    [J]. PLPV'10: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON PROGRAMMING LANGUAGES MEETS PROGRAM VERIFICATION, 2010, : 15 - 26
  • [5] A lightweight approach to datatype-generic rewriting
    Van Noort, Thomas
    Yakushev, Alexey Rodriguez
    Holdermans, Stefan
    Jeuring, Johan
    Heeren, Bastiaan
    Magalhaes, Jose Pedro
    [J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2010, 20 : 375 - 413
  • [6] A Lightweight Approach to Datatype-Generic Rewriting
    van Noort, Thomas
    Rodriguez, Alexey
    Holdermans, Stefan
    Jeuring, Johan
    Heeren, Bastiaan
    [J]. WGP'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN WORKSHOP ON GENERIC PROGRAMMING, 2008, : 13 - 24
  • [7] A Formal Comparison of Approaches to Datatype-Generic Programming
    Magalhaes, Jose Pedro
    Loeh, Andres
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (76): : 50 - 67
  • [8] Datatype-Generic Programming Meets Elaborator Reflection
    Ko, Hsiang-Shang
    Chen, Liang-Ting
    Lin, Tzu-Chi
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (ICFP):
  • [9] System F-omega with Equirecursive Types for Datatype-Generic Programming
    Cai, Yufei
    Giarrusso, Paolo G.
    Ostermann, Klaus
    [J]. ACM SIGPLAN NOTICES, 2016, 51 (01) : 30 - 43
  • [10] Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning
    Mu, Shin-Cheng
    Lyu, Yu-Han
    Morihata, Akimasa
    [J]. WGP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON GENERIC PROGRAMMING, 2010, : 97 - 108
12345