Representing model theory in a type-theoretical logical framework (Q654913): Difference between revisions

From MaRDI portal
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
(15 intermediate revisions by 3 users not shown)
Property / describes a project that uses
 
Property / describes a project that uses: Mizar / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Hets / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ALF / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: gaia / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Flyspeck / 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: Isabelle/HOL / 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: Automath / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: OMDoc / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL Light / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Nuprl / 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.1016/j.tcs.2011.03.022 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2046048646 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Crafting a Proof Assistant / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3937387 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Encoding modal logics in logical frameworks / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2722016 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3889024 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Some Domain Theory and Denotational Semantics in Coq / rank
 
Normal rank
Property / cites work
 
Property / cites work: Combining Type Theory and Untyped Set Theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Intuitionistic model constructions and normalization proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5565113 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The calculus of constructions / rank
 
Normal rank
Property / cites work
 
Property / cites work: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5610115 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof Systems for Institutional Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4723263 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Institutions: abstract model theory for specification and programming / rank
 
Normal rank
Property / cites work
 
Property / cites work: Consistency of the Continuum Hypothesis. (AM-3) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Institution morphisms / rank
 
Normal rank
Property / cites work
 
Property / cites work: A framework for defining logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Representing Model Theory in a Type-Theoretical Logical Framework / rank
 
Normal rank
Property / cites work
 
Property / cites work: Structured theory presentations and logic representations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Project Abstract: Logic Atlas and Integrator (LATIN) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4215784 / rank
 
Normal rank
Property / cites work
 
Property / cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES / rank
 
Normal rank
Property / cites work
 
Property / cites work: Towards a mechanized metatheory of standard ML / rank
 
Normal rank
Property / cites work
 
Property / cites work: Refinement Types as Proof Irrelevance / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3032225 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5311059 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4099613 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4360856 / rank
 
Normal rank
Property / cites work
 
Property / cites work: HOLCF = HOL + LCF / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4362967 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4435474 / 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: Q4790669 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle. A generic theorem prover / rank
 
Normal rank
Property / cites work
 
Property / cites work: Structural cut elimination. I: Intuitionistic and classical logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3666260 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3265664 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Mizar’s Soft Type System / rank
 
Normal rank

Latest revision as of 19:26, 4 July 2024

scientific article
Language Label Description Also known as
English
Representing model theory in a type-theoretical logical framework
scientific article

    Statements

    Representing model theory in a type-theoretical logical framework (English)
    0 references
    0 references
    0 references
    23 December 2011
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    logical framework
    0 references
    model-theoretic semantics
    0 references
    proof-theoretic semantics
    0 references
    first-order logic
    0 references
    Twelf module system
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references