A Formal Proof of the Strong Normalization Theorem for System T in Agda (Q6118750): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
ReferenceBot (talk | contribs)
Changed an Item
 
(One intermediate revision by one other user not shown)
Property / Wikidata QID
 
Property / Wikidata QID: Q122402818 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Normalization for the Simply-Typed Lambda-Calculus in Twelf / rank
 
Normal rank
Property / cites work
 
Property / cites work: POPLMark reloaded: Mechanizing proofs by logical relations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3728878 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5667469 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The locally nameless representation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formal metatheory of the lambda calculus using Stoughton's substitution / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2871864 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3994895 / rank
 
Normal rank
Property / cites work
 
Property / cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3522248 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Substitution revisited / rank
 
Normal rank
Property / cites work
 
Property / cites work: Intensional interpretations of functionals of finite type I / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nominal unification / rank
 
Normal rank
Property / cites work
 
Property / cites work: Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda / rank
 
Normal rank

Latest revision as of 13:18, 27 August 2024

scientific article; zbMATH DE number 7810647
Language Label Description Also known as
English
A Formal Proof of the Strong Normalization Theorem for System T in Agda
scientific article; zbMATH DE number 7810647

    Statements

    Identifiers

    0 references
    0 references
    0 references
    0 references