Pages that link to "Item:Q769601"

The following pages link to Combinatory logic. With two sections by William Craig. (Q769601):

Displaying 50 items.

• The future of logic: foundation-independence (Q263104) (← links)
• A decidable theory of type assignment (Q365669) (← links)
• Intuitionistic completeness of first-order logic (Q392280) (← links)
• How to assign ordinal numbers to combinatory terms with polymorphic types (Q453195) (← links)
• Type-theoretic logic with an operational account of intensionality (Q514081) (← links)
• A logical analysis of the Anselm's \textit{Unum argumentum} (from \textit{Proslogion}) (Q523297) (← links)
• Cut-elimination in the strict intersection type assignment system is strongly normalizing (Q558418) (← links)
• Spaces with combinators (Q688513) (← links)
• The \(\lambda \)-calculus and the unity of structural proof theory (Q733755) (← links)
• A new theory of quantifiers and term connectives (Q735412) (← links)
• About systems of equations, X-separability, and left-invertibility in the \(\lambda\)-calculus (Q752684) (← links)
• Type inference with recursive types: Syntax and semantics (Q756435) (← links)
• Une nouvelle C\(\beta\)-réduction dans la logique combinatoire (Q762137) (← links)
• Propositions and specifications of programs in Martin-Löf's type theory (Q800719) (← links)
• The absence and the presence of fixed point combinators (Q807612) (← links)
• Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result (Q809993) (← links)
• A variadic extension of Curry's fixed-point combinator (Q812092) (← links)
• Types of I-free hereditary right maximal terms (Q812102) (← links)
• An epistemic logic for becoming informed (Q833038) (← links)
• From IF to BI. A tale of dependence and separation (Q833040) (← links)
• Innovations in computational type theory using Nuprl (Q865639) (← links)
• SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953) (← links)
• Do-it-yourself type theory (Q911744) (← links)
• The heart of intersection type assignment: Normalisation proofs revisited (Q930869) (← links)
• A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
• Implementing a computer algebra system in Haskell (Q990498) (← links)
• Schönfinkel-type operators for classical logic (Q993497) (← links)
• A solution to Curry and Hindley's problem on combinatory strong reduction (Q1014284) (← links)
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
• Relevant predication. I: The formal theory (Q1099150) (← links)
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models (Q1102936) (← links)
• Polymorphic type inference and containment (Q1110312) (← links)
• The word problem for Smullyan's lark combinator is decidable (Q1114668) (← links)
• Equivalence of bar recursors in the theory of functionals of finite type (Q1115867) (← links)
• Type theory and concurrency (Q1124322) (← links)
• Condensed detachment is complete for relevance logic: A computer-aided proof (Q1181717) (← links)
• Coquand's calculus of constructions: A mathematical foundation for a proof development system (Q1201296) (← links)
• The systematic construction of a one-combinator basis for lambda-terms (Q1203131) (← links)
• Principal types of BCK-lambda-terms (Q1208417) (← links)
• Combinator operations (Q1227001) (← links)
• Completeness of the normal typed fragment of the \(\lambda\)-system \(U\) (Q1237066) (← links)
• A new way of normalizing intuitionistic propositional logic (Q1237067) (← links)
• Synchronization and computing capabilities of linear asynchronous structures (Q1242906) (← links)
• Positive logic and \(\lambda\)-constants (Q1252340) (← links)
• Some models of combinatory logic (Q1259579) (← links)
• Proof-functional connectives and realizability (Q1330311) (← links)
• Non-well-founded sets via revision rules (Q1337508) (← links)
• The ``relevance'' of intersection and union types (Q1381437) (← links)
• Revisiting the notion of function (Q1394989) (← links)