On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain

被引：0
|
作者：
S. D. Meshveliani
机构：
[1] Ailamazyan Program Systems Institute,
[2] Russian Academy of Sciences,undefined
来源：
Programming and Computer Software | 2020年 / 46卷
关键词：
D O I：
暂无
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：110 / 119
页数：9
相关论文
共 50 条
  • [1] On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
    Meshveliani, S. D.
    PROGRAMMING AND COMPUTER SOFTWARE, 2020, 46 (02) : 110 - 119
  • [2] A machine-checked correctness proof for Pastry
    Azmy, Noran
    Merz, Stephan
    Weidenbach, Christoph
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 64 - 80
  • [3] A Machine-Checked Proof of the Odd Order Theorem
    Gonthier, Georges
    Asperti, Andrea
    Avigad, Jeremy
    Bertot, Yves
    Cohen, Cyril
    Garillot, Francois
    Le Roux, Stephane
    Mahboubi, Assia
    O'Connor, Russell
    Biha, Sidi Ould
    Pasca, Ioana
    Rideau, Laurence
    Solovyev, Alexey
    Tassi, Enrico
    Thery, Laurent
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 163 - 179
  • [4] A machine-checked theory of floating point arithmetic
    Harrison, J
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 1999, 1690 : 113 - 130
  • [5] TRACKING DESIGN CHANGES WITH FORMAL MACHINE-CHECKED PROOF
    CURZON, P
    COMPUTER JOURNAL, 1995, 38 (02): : 91 - 100
  • [6] A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
    Kellison, Ariel
    PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 265 - 273
  • [7] Machine-Checked Proof-Theory for Propositional Modal Logics
    Dawson, Jeremy E.
    Gore, Rajeev
    Wu, Jesse
    ADVANCES IN PROOF THEORY, 2016, 28 : 173 - 243
  • [8] A machine-checked soundness proof for an efficient verification condition generator
    Vogels, Frédéric
    Jacobs, Bart
    Piessens, Frank
    Proceedings of the ACM Symposium on Applied Computing, 2010, : 2517 - 2522
  • [9] A Machine-Checked Proof of Security for AWS Key Management Service
    Almeida, Jose Bacelar
    Barbosa, Manuel
    Barthe, Gilles
    Campagna, Matthew
    Cohen, Ernie
    Gregoire, Benjamin
    Pereira, Vitor
    Portela, Bernardo
    Strub, Pierre-Yves
    Tasiran, Serdar
    PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, : 63 - 78
  • [10] A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
    van der Weegen, Eelis
    McKinna, James
    TYPES FOR PROOFS AND PROGRAMS, 2009, 5497 : 256 - 271
12345