A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
ReferenceBot (talk | contribs)
Changed an Item
 
(4 intermediate revisions by 3 users not shown)
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 / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / cites work
 
Property / cites work: The lambda calculus. Its syntax and semantics. Rev. ed. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proving Properties of Programs by Structural Induction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Some Properties of Conversion / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5565113 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5667469 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Primitive recursion for higher-order abstract syntax / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2703747 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A new approach to abstract syntax with variable binding / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4783299 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Residual theory in λ-calculus: a formal development / rank
 
Normal rank
Property / cites work
 
Property / cites work: Completion of a Set of Rules Modulo a Set of Equations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3918095 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4274979 / rank
 
Normal rank
Property / cites work
 
Property / cites work: An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Some lambda calculus and type theory formalized / 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: A mechanical proof of the Church-Rosser theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Substitution revisited / rank
 
Normal rank
Property / cites work
 
Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2778886 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4518890 / rank
 
Normal rank
links / mardi / namelinks / mardi / name
 

Latest revision as of 08:57, 6 June 2024

scientific article
Language Label Description Also known as
English
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
scientific article

    Statements

    A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (English)
    0 references
    0 references
    0 references
    19 August 2003
    0 references
    \({\lambda}\)-Calculus
    0 references
    Structural induction and recursion
    0 references
    Confluence
    0 references
    Theorem proving
    0 references
    Barendregt's Variable Convention
    0 references

    Identifiers