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 条
  • [41] A machine-checked model for a java']java-like language, virtual machine, and compiler
    Klein, Gerwin
    Nipkow, Tobias
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006, 28 (04): : 619 - 695
  • [42] Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
    Meier, Simon
    Cremers, Cas
    Basin, David
    2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 231 - 245
  • [43] A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation
    Eldefrawy, Karim
    Pereira, Vitor
    PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, : 851 - 868
  • [44] Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Estaji, Ehsan
    Gjosteen, Kristian
    Haines, Thomas
    Ryan, Peter Y. A.
    Ronne, Peter B.
    Solberg, Morten Rotvold
    2022 IEEE 35TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2022), 2022, : 335 - 347
  • [45] Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory
    Copello, Ernesto
    Szasz, Nora
    Tasistro, Alvaro
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2018, 338 : 79 - 95
  • [46] Java']Java and the Java']Java Memory Model - A Unified, Machine-Checked Formalisation
    Lochbihler, Andreas
    PROGRAMMING LANGUAGES AND SYSTEMS, 2012, 7211 : 497 - 517
  • [47] Towards machine-checked compiler correctness for higher-order pure functional languages
    Lester, D
    Mintchev, S
    COMPUTER SCIENCE LOGIC, 1995, 933 : 369 - 381
  • [48] Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
    Chargueraud, Arthur
    Pottier, Francois
    INTERACTIVE THEOREM PROVING, 2015, 9236 : 137 - 153
  • [49] A Machine Checked Soundness Proof for an Intermediate Verification Language
    Vogels, Frederic
    Jacobs, Bart
    Piessens, Frank
    SOFSEM 2009-THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2009, 5404 : 570 - 581
  • [50] Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols
    Barthe, Gilles
    Crespo, Juan Manuel
    Lakhnech, Yassine
    Schmidt, Benedikt
    ADVANCES IN CRYPTOLOGY - EUROCRYPT 2015, PT II, 2015, 9057 : 689 - 718
12345