Pages that link to "Item:Q801050"

The following pages link to The lambda calculus. Its syntax and semantics. Rev. ed. (Q801050):

Displaying 50 items.

• Retractions of dI-domains as a model for Type:Type (Q805221) (← links)
• Simple consequence relations (Q809992) (← links)
• A variadic extension of Curry's fixed-point combinator (Q812092) (← links)
• A calculus of coroutines (Q817847) (← links)
• The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609) (← links)
• Simplifying the signature in second-order unification (Q843951) (← links)
• Productivity of stream definitions (Q846366) (← links)
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
• An initial algebra approach to term rewriting systems with variable binders (Q853743) (← links)
• Expressing combinatory reduction systems derivations in the rewriting calculus (Q857913) (← links)
• Type checking a multithreaded functional language with session types (Q859841) (← links)
• Weak typed Böhm theorem on IMLL (Q866556) (← links)
• Resource operators for \(\lambda\)-calculus (Q876041) (← links)
• On tree automata that certify termination of left-linear term rewriting systems (Q876043) (← links)
• Fair ambients (Q877172) (← links)
• A \(\rho\)-calculus of explicit constraint application (Q880989) (← links)
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953) (← links)
• Theory of interaction (Q896903) (← links)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
• A synthetic axiomatization of map theory (Q906269) (← links)
• A logic of abstraction related to finite constructive number classes (Q910401) (← links)
• A category-theoretic characterization of functional completeness (Q912587) (← links)
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) (Q923069) (← links)
• The logic of message-passing (Q923880) (← links)
• The heart of intersection type assignment: Normalisation proofs revisited (Q930869) (← links)
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage (Q930871) (← links)
• An irregular filter model (Q930872) (← links)
• On generic context lemmas for higher-order calculi with sharing (Q960863) (← links)
• On the observational theory of the CPS-calculus (Q968276) (← links)
• External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
• On the membership problem for non-linear abstract categorial grammars (Q972435) (← links)
• A faithful representation of non-associative Lambek grammars in abstract categorial grammars (Q972436) (← links)
• A semantic proof of polytime soundness of light affine logic (Q987375) (← links)
• On the confluence of lambda-calculus with conditional rewriting (Q987976) (← links)
• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets (Q1006642) (← links)
• A solution to Curry and Hindley's problem on combinatory strong reduction (Q1014284) (← links)
• On structural properties of eta-expansions of identity (Q1014452) (← links)
• From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality (Q1021567) (← links)
• Applications of infinitary lambda calculus (Q1021568) (← links)
• On the completeness of order-theoretic models of the \(\lambda \)-calculus (Q1021569) (← links)
• A construction of one-point bases in extended lambda calculi (Q1029098) (← links)
• CPS-translation as adjoint (Q1044830) (← links)
• Strong normalization property for second order linear logic (Q1044837) (← links)
• A characterization of F-complete type assignments (Q1089331) (← links)
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models (Q1102936) (← links)
• Substitution revisited (Q1106190) (← links)
• Algebra of constructions. I. The word problem for partial algebras (Q1107515) (← links)
• Principal type scheme and unification for intersection type discipline (Q1110311) (← links)
• Polymorphic type inference and containment (Q1110312) (← links)
• Conditional rewrite rules: Confluence and termination (Q1111368) (← links)