Pages that link to "Item:Q1850959"
From MaRDI portal
The following pages link to A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions (Q1850959):
Displaying 17 items.
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Kripke models for classical logic (Q636371) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus (Q672060) (← links)
- Formalizing strong normalization proofs of explicit substitution calculi in ALF (Q1810858) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- Strongly typed term representations in Coq (Q2392480) (← links)
- A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
- Type-level computation using narrowing in \(\Omega\)mega (Q2866338) (← links)
- Normalization for the simply-typed lambda-calculus in Twelf (Q2871835) (← links)
- An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus (Q2915182) (← links)
- The Expansion Problem in Lambda Calculi with Explicit Substitution (Q3549313) (← links)
- Big-step normalisation (Q3638919) (← links)
- (Q4323124) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search (Q5236550) (← links)
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (Q5747746) (← links)
