A formalization and proof checker for Isabelle's metalogic (Q2108191)

From MaRDI portal
Revision as of 02:21, 17 December 2024 by Import241208061232 (talk | contribs) (Normalize DOI.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
A formalization and proof checker for Isabelle's metalogic
scientific article

    Statements

    title
    A formalization and proof checker for Isabelle's metalogic (English)
    0 references
    author
    Simon Roßkopf
    0 references
    Tobias Nipkow
    0 references
    publication date
    19 December 2022
    0 references
    zbMATH Keywords
    theorem proving
    0 references
    higher-order logic
    0 references
    Isabelle
    0 references
    proof checker
    0 references
    metalogic
    0 references
    describes a project that uses
    Isabelle
    0 references
    Isabelle/HOL
    0 references
    HOL Zero
    0 references
    Lifting
    0 references
    CakeML
    0 references
    Twelf
    0 references
    Elf
    0 references
    OpenTheory
    0 references
    Coq
    0 references
    Milawa
    0 references
    Metamath Zero
    0 references
    Transfer
    0 references
    Nominal Isabelle
    0 references
    Jitawa
    0 references
    cites work
    Concrete Semantics
    0 references
    Q2754030
    0 references
    Q3075242
    0 references
    Q4246942
    0 references
    Q3204068
    0 references
    Q4274997
    0 references
    Q4736387
    0 references
    CakeML
    0 references

    Identifiers

    Mathematics Subject Classification ID
    68V15
    0 references
    03B35
    0 references
    68V20
    0 references
    zbMATH DE Number
    7634129
    0 references
    OpenAlex ID
    W4312126060
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q2108191&oldid=38883732"
    Powered by MediaWiki