A formalization and proof checker for Isabelle's metalogic (Q2108191): Difference between revisions

From MaRDI portal
← Older edit
Added link to MaRDI item.
Import241208061232 (talk | contribs)
1,022,404 edits
Normalize DOI.
 
(17 intermediate revisions by 4 users not shown)
Property / DOI
 
Property / DOI: 10.1007/s10817-022-09648-w / rank
Normal rank
 
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL Zero / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Lifting / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: CakeML / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Twelf / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Elf / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: OpenTheory / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Coq / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Milawa / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Metamath Zero / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Transfer / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Nominal Isabelle / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Jitawa / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/s10817-022-09648-w / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W4312126060 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Towards Self-verification of HOL Light / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle. A generic theorem prover / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Concrete Semantics / rank
 
Normal rank
Property / cites work
 
Property / cites work: The foundation of a generic theorem prover / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754030 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle's metalogic: formalization and proof checker / rank
 
Normal rank
Property / cites work
 
Property / cites work: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation / rank
 
Normal rank
Property / cites work
 
Property / cites work: A verified proof checker for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Consistent Foundation for Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Comprehending Isabelle/HOL’s Consistency / rank
 
Normal rank
Property / cites work
 
Property / cites work: A consistent foundation for Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: HOL Zero’s Solutions for Pollack-Inconsistency / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3075242 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4246942 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Metamath Zero: designing a theorem prover prover / rank
 
Normal rank
Property / cites work
 
Property / cites work: The reflective Milawa theorem prover is sound (down to the machine code that runs it) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nominal techniques in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: A formalized general theory of syntax with bindings: extended version / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3204068 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: More Church-Rosser proofs (in Isabelle/HOL) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4274997 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Type Reconstruction for Type Classes / rank
 
Normal rank
Property / cites work
 
Property / cites work: Constructive Type Classes in Isabelle / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4736387 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Data Refinement in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Seventy-five problems for testing automatic theorem provers / rank
 
Normal rank
Property / cites work
 
Property / cites work: CakeML / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Isabelle Collections Framework / rank
 
Normal rank
Property / cites work
 
Property / cites work: Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1007/S10817-022-09648-W / rank
 
Normal rank

Latest revision as of 02:21, 17 December 2024

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