scientific article; zbMATH DE number 3993540
From MaRDI portal
Publication:4722037
zbMath0614.03014MaRDI QIDQ4722037
Jonathan P. Seldin, J. Roger Hindley
Publication date: 1986
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40)
Related Items
Some analytic features of algebraic data, Nominal lambda calculus: an internal language for FM-Cartesian closed categories, Eager functions as processes, \(F\)-semantics for type assignment systems, A computable expression of closure to efficient causation, Eta-conversion for the languages of explicit substitutions, Self-quotation in a typed, intensional lambda-calculus, Third order matching is decidable, The Church-Rosser theorem and quantitative analysis of witnesses, Hierarchical addressing in symbolic computation, Parametric parameter passing \(\lambda\)-calculus, A note on the proof theory of the \(\lambda \Pi\)-calculus, Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends, Formalizing non-termination of recursive programs, \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule, Lambda terms definable as combinators, Totality in applicative theories, Strong normalization from weak normalization in typed \(\lambda\)-calculi, Normal forms in combinatory logic, NP-completeness of a combinator optimization problem, A functional computation model for the duality of two-variable lambda-Boolean functions, BCK-combinators and linear \(\lambda\)-terms have types, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, On pseudo-c\(\beta\) normal form in combinatory logic, A reduction rule for Peirce formula, On a conjecture of Bergstra and Tucker, The ``relevance of intersection and union types, Higher-order rewrite systems and their confluence, Combinatory weak reduction in lambda calculus, A process calculus with finitary comprehended terms, Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters, \(c\beta\)-Machine with \(\lambda \beta\)-reduction, Revisiting the notion of function, Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Alpha equivalence equalities, A logic of abstraction related to finite constructive number classes, A category-theoretic characterization of functional completeness, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, Theories with self-application and computational complexity., The semantics of entailment omega, Subtyping can have a simple semantics, Intensional computation with higher-order functions, Implementing the `Fool's model' of combinatory logic, Factorization in call-by-name and call-by-value calculi via linear logic, The self-reduction in lambda calculus, Intersection type assignment systems with higher-order algebraic rewriting, Two beta-equal lambda-I-terms with no types in common, Most general first order theorems are not recursively enumerable, A combinatory logic approach to higher-order E-unification, Conditional rewriting logic as a unified model of concurrency, Decision problems for propositional linear logic, The converse principal type-scheme theorem in lambda calculus, Linear logic, coherence and dinaturality, Functional interpretations of feasibly constructive arithmetic, A simple proof of a theorem of Statman, Intersection types for combinatory logic, Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category, A logical analysis of the Anselm's \textit{Unum argumentum} (from \textit{Proslogion}), Coquand's calculus of constructions: A mathematical foundation for a proof development system, Types with intersection: An introduction, Unification under a mixed prefix, Partial inductive definitions as type-systems for \(\lambda\)-terms, Definition and basic properties of the Deva meta-calculus, Principal types of BCK-lambda-terms, How to decide the lark, A proof-theoretic characterization of the basic feasible functionals, Computability in higher types, P\(\omega\) and the completeness of type assignment, Abstract deduction and inferential models for type theory, A direct proof of the confluence of combinatory strong reduction, Abstraction problems in combinatory logic: A compositive approach, Type inference with recursive types: Syntax and semantics, Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete, Infinite \(\lambda\)-calculus and types, On functions preserving levels of approximation: A refined model construction for various lambda calculi, The foundation of a generic theorem prover, Higher-order unification revisited: Complete sets of transformations, Perpetual reductions in \(\lambda\)-calculus, Generalized filter models, A Gentzen-style sequent calculus of constructions with expansion rules, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Program development schemata as derived rules, Efficient multi-variate abstraction using an array representation for combinators., On the undecidability of second-order unification, Structuring metatheory on inductive definitions, Inductive synthesis of recursive processes from logical properties, Higher-order substitutions, Parallel beta reduction is not elementary recursive, Implementing tactics and tacticals in a higher-order logic programming language, The kernel strategy and its use for the study of combinatory logic, Experimenting with Isabelle in ZF set theory, Kripke-style models for typed lambda calculus, Computational foundations of basic recursive function theory, General recursive functions in a very simply interpretable typed \(\lambda\)-calculus, Combinatory reduction systems: Introduction and survey, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Variables and scopes considered formally, Communication errors in the \(\pi\)-calculus are undecidable, Types of I-free hereditary right maximal terms, An algebraic semantics of higher-order types with subtypes, Admissibility of cut in LC with fixed point combinator, Formal metatheory of the lambda calculus using Stoughton's substitution, Termination of combined (rewrite and λ-calculus) systems, Extended term rewriting systems, Typed equivalence, type assignment, and type containment, Higher-order unification, polymorphism, and subsorts, The Senses of Functions in the Logic of Sense and Denotation, On the role of implication in formal logic, An investigation into functions as processes, Higher-order unification via combinators, The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL, A combinatory account of internal structure, Higher-order unification with dependent function types, Open problems in rewriting, A termination ordering for higher order rewrite systems, Higher-order families, Trees from Functions as Processes, Unnamed Item, Systems of illative combinatory logic complete for first-order propositional and predicate calculus, Uniqueness of normal proofs of minimal formulas, Construction of the model of the lambda calculus system with algebraic operators, Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions, From operational semantics to abstract machines, Categorical models for non-extensional λ-calculi and combinatory logic, Combinatory logic and the semantics of substructural logics, Structuring metatheory on inductive definitions, Constructive natural deduction and its ‘ω-set’ interpretation, On adding (ξ) to weak equality in combinatory logic, The Mathematical Work of S.C.Kleene, Principal type-schemes and condensed detachment, Higher-order order-sorted algebras, Wrapper semantics of an object-oriented programming language with state, Principal type-schemes of BCI-lambda-terms, Higher order disunification: Some decidable cases, Higher order conditional rewriting and narrowing, Higher-order narrowing with convergent systems, Unnamed Item, On extensibility of proof checkers, A correct-by-construction conversion from lambda calculus to combinatory logic, The placeholder view of assumptions and the Curry-Howard correspondence, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Simultaneous substitution in the typed lambda calculus, Abstract machines, optimal reduction, and streams, Unnamed Item, Proposal for a natural formalization of functional programming concepts, Weak polymorphism can be sound, Decidability of bounded higher-order unification, Enhancing dependency pair method using strong computability in simply-typed term rewriting, Logic and Geometry of Agents in Agent-Based Modeling, The representational adequacy of <scp>Hybrid</scp>, Collapsing partial combinatory algebras, Decidability of all minimal models, The Church-Rosser property in symmetric combinatory logic, Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them, 2002–2003 Winter Meeting of the Association for Symbolic Logic, Abstraction in algorithmic logic, Alonzo church:his life, his work and some of his miracles, A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains, Type system in programming languages, A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG, An Introduction to the Lambda Calculus, Abstract λ-Calculus Machines, Introduction to Type Theory, MBase: Representing knowledge and context for the integration of mathematical software systems, A type-theoretic approach to program development, Some results on combinators in the system TRC, Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models, Completeness of type assignment systems with intersection, union, and type quantifiers, On the proof theory of Coquand's calculus of constructions, Call-by-value Solvability, Unnamed Item, Cooperation of Algebraic Constraint Domains in Higher-Order Functional and Logic Programming, RPO, Second-Order Contexts, and λ-Calculus, Types for Hereditary Head Normalizing Terms, Decidable higher-order unification problems, Higher-Order Multi-Valued Resolution, On Some Semi-constructive Theories Related to Kripke–Platek Set Theory, BUNDER’S PARADOX, The Church-Rosser property in dual combinatory logic, Natural Deduction for Equality: The Missing Entity, π-RED+ An interactive compiling graph reduction system for an applied λ-calculus, A Glimpse of $$ \sum_{3} $$-elementarity, A structural approach to reversible computation, Extending the first-order theory of combinators with self-referential truth, Quantifier elimination and parametric polymorphism in programming languages, The complexity of type inference for higher-order typed lambda calculi, Higher-order narrowing with definitional trees
