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 条
  • [1] Nominal techniques in Isabelle/HOL
    Urban, Christian
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 327 - 356
  • [2] Nominal techniques in Isabelle/HOL
    Urban, C
    Tasson, C
    AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 38 - 53
  • [3] Nominal Techniques in Isabelle/HOL
    Christian Urban
    Journal of Automated Reasoning, 2008, 40 : 327 - 356
  • [4] A recursion combinator for nominal datatypes implemented in Isabelle/HOL
    Urban, Christian
    Berghofer, Stefan
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 498 - 512
  • [5] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [6] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [7] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
  • [8] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
  • [9] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [10] Data Refinement in Isabelle/HOL
    Haftmann, Florian
    Krauss, Alexander
    Kuncar, Ondrej
    Nipkow, Tobias
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 100 - 115
12345