Tutorial on interactive theorem proving using type theory

被引：0
|
作者：
Howe, DJ [1 ]
机构：
[1] Bell Labs, Murray Hill, NJ 07974 USA
来源：
COMPUTER SCIENCE LOGIC, PROCEEDINGS | 1999年 / 1683卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
引用
收藏
页码：578 / 578
页数：1
相关论文
共 50 条
  • [21] Formal verification of Matrix based MATLAB models using interactive theorem proving
    Gauhar, Ayesha
    Rashid, Adnan
    Hasan, Osman
    Bispo, Joao
    Cardoso, Joao M. P.
    PEERJ COMPUTER SCIENCE, 2021, 7 : 1 - 21
  • [22] Theorem proving for a theory of shape graphs
    Zhang Y.
    Chen Y.-Y.
    Li Z.-P.
    Jisuanji Xuebao/Chinese Journal of Computers, 2016, 39 (12): : 2460 - 2480
  • [23] A SYNTHESIS OF THE PROCEDURAL AND DECLARATIVE STYLES OF INTERACTIVE THEOREM PROVING
    Wiedijk, Freek
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
  • [24] Interactive theorem proving: An empirical study of user activity
    Aitken, JS
    Gray, P
    Melham, T
    Thomas, M
    JOURNAL OF SYMBOLIC COMPUTATION, 1998, 25 (02) : 263 - 284
  • [25] Shared-Memory Multiprocessing for Interactive Theorem Proving
    Wenzel, Makarius
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 418 - 434
  • [26] Meta-level verification of the quality of medical guidelines using interactive theorem proving
    Hommersom, A
    Lucas, P
    Balser, M
    LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, 3229 : 654 - 666
  • [27] Evaluation of an interactive tutorial for teaching the central limit theorem
    Aberson, CL
    Berger, DE
    Healy, MR
    Kyle, DJ
    Romero, VL
    TEACHING OF PSYCHOLOGY, 2000, 27 (04) : 289 - 291
  • [28] Source-level proof reconstruction for interactive theorem proving
    Paulson, Lawrence C.
    Susanto, Kong Woei
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2007, 4732 : 232 - +
  • [29] 14th International Conference on Interactive Theorem Proving
    Naumowicz, Adam
    Thiemann, René
    Leibniz International Proceedings in Informatics, LIPIcs, 2023, 268
  • [30] Survey on Interactive Theorem Proving Based Concurrent Program Verification
    Wang Z.-Y.
    Wu S.-S.
    Cao Q.-X.
    Ruan Jian Xue Bao/Journal of Software, 2024, 35 (09):
12345