Nominal techniques in isabelle/HOL

被引：0
|
作者：
Urban, Christian [1 ]
机构：
[1] Technical University Munich, Munich, Germany
来源：
Journal of Automated Reasoning | 2008年 / 40卷 / 04期
关键词：
Particle accelerators;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Journal article (JA)
引用
收藏
页码：327 / 356
相关论文
共 50 条
  • [31] On the mechanization of real analysis in Isabelle/HOL
    Fleuriot, JD
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 145 - 161
  • [32] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
  • [33] Imperative functional programming with Isabelle/HOL
    Bulwahn, Lukas
    Krauss, Alexander
    Haftmann, Horian
    Erkoek, Levent
    Matthews, John
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 134 - +
  • [34] Stateful Protocol Composition in Isabelle/HOL
    Hess, Andreas V.
    Modersheim, Sebastian A.
    Brucker, Achim D.
    ACM TRANSACTIONS ON PRIVACY AND SECURITY, 2023, 26 (03)
  • [35] Weak alternating automata in Isabelle/HOL
    Merz, S
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 424 - 441
  • [36] Bounded Model Generation for Isabelle/HOL
    Weber, Tjark
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (03) : 103 - 116
  • [37] Formalizing provable anonymity in Isabelle/HOL
    Li, Yongjian
    Pang, Jun
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (02) : 255 - 282
  • [38] Formalizing rewriting introduction on Isabelle/HOL
    Kimura Y.
    Aoto T.
    Computer Software, 2020, 37 (02) : 104 - 119
  • [39] Algebras for Program Correctness in Isabelle/HOL
    Armstrong, Alasdair
    Gomes, Victor Bf
    Struth, Georg
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014), 2014, 8428 : 49 - 64
  • [40] Lyndon Words Formalized in Isabelle/HOL
    Holub, Stepan
    Starosta, Stepan
    DEVELOPMENTS IN LANGUAGE THEORY, DLT 2021, 2021, 12811 : 217 - 228
12345