scientific article; zbMATH DE number 3280068
From MaRDI portal
Publication:5565113
zbMath0175.27601MaRDI QIDQ5565113
Publication date: 1968
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Variants of the basic calculus of constructions, On the \(\lambda Y\) calculus, A characterization of F-complete type assignments, Parametric parameter passing \(\lambda\)-calculus, The Girard-Reynolds isomorphism, Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends, Lambda terms definable as combinators, Intersection type assignment systems, On completeness and cocompleteness in and around small categories, Word operation definable in the typed \(\lambda\)-calculus, Partial combinatory algebra and generalized numberings, Normalization results for typeable rewrite systems, Strong normalization from weak normalization in typed \(\lambda\)-calculi, One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus, Substitution revisited, The calculus of constructions, Principal type scheme and unification for intersection type discipline, Full abstraction and recursion, Conditional rewrite rules: Confluence and termination, BCK-combinators and linear \(\lambda\)-terms have types, Ternary relations and relevant semantics, On pseudo-c\(\beta\) normal form in combinatory logic, The Girard-Reynolds isomorphism (second edition), Developing developments, Indexings of subrecursive classes, From types to sets, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, A type-assignment of linear erasure and duplication, On the strong normalisation of intuitionistic natural deduction with permutation-conversions, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Invertible terms in the lambda calculus, Alpha equivalence equalities, An efficient interpreter for the lambda-calculus, Constructive system for automatic program synthesis, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, The IO- and OI-hierarchies, Pre-recursive categories, A characterization of lambda definable tree operations, On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems, A binary modal logic for the intersection types of lambda-calculus., The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction, Representing model theory in a type-theoretical logical framework, Krivine machines and higher-order schemes, Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda, Intensional computation with higher-order functions, A combinatory logic approach to higher-order E-unification, Lambda abstraction algebras: representation theorems, Conditional rewriting logic as a unified model of concurrency, On the representation of semigroups and other congruences in the lambda calculus, Projections for infinitary rewriting, The search for a reduction in combinatory logic equivalent to \(\lambda \beta\)-reduction. II., Complete restrictions of the intersection type discipline, On randomised strategies in the \(\lambda \)-calculus, On abstract normalisation beyond neededness, Intersection types for combinatory logic, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, How to decide the lark, External and internal syntax of the \(\lambda \)-calculus, From distributed coordination to field calculus and aggregate computing, Call-by-name, call-by-value and the \(\lambda\)-calculus, An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus, Computability in higher types, P\(\omega\) and the completeness of type assignment, On sets of solutions to combinator equations, Quantifier-complete categories, Functionals computable in series and in parallel, An algebraic framework for minimum spanning tree problems, Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus, A global representation of the recursive functions in the \(\lambda\)- calculus, A direct proof of the confluence of combinatory strong reduction, N. G. de Bruijn's contribution to the formalization of mathematics, A discrimination algorithm inside \(\lambda -\beta\)-calculus, Intuitionistic propositional logic is polynomial-space complete, Abstraction problems in combinatory logic: A compositive approach, The discrimination theorem holds for combinatory weak reduction, Typing and computational properties of lambda expressions, From constructivism to computer science, Expressive power of typed and type-free programming languages, A set of combinators for abstraction in linear space, A construction of one-point bases in extended lambda calculi, Towards a computation system based on set theory, Sequential evaluation strategies for parallel-or and related reduction systems, A finite equational axiomatization of the functional algebras for the lambda calculus, Perpetual reductions in \(\lambda\)-calculus, Linear logic by levels and bounded time complexity, The completeness theorem for typing lambda-terms, On the algebraic models of lambda calculus, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, Principal type schemes for an extended type theory, Theory of symbolic expressions. I, Realizability and intuitionistic logic, Reduction graphs in the lambda calculus, Completeness of type assignment in continuous lambda models, Efficient multi-variate abstraction using an array representation for combinators., Descendants and origins in term rewriting., \(\lambda\)-definability of free algebras, Some examples of non-existent combinators, Systems of combinatory logic related to Quine's `New Foundations', Combining type disciplines, The connection between an event structure semantics and an operational semantics for TCSP, Formal metatheory of the lambda calculus using Stoughton's substitution, Higher-order unification via combinators, Unnamed Item, Stratification and cut-elimination, A higher-order calculus and theory abstraction, Unnamed Item, Infinite objects in type theory, Projections for infinitary rewriting (extended version), Adding Negation to Lambda Mu, Realizability algebras III: some examples, Unnamed Item, Unnamed Item, Unnamed Item, Proposal for a natural formalization of functional programming concepts, Unnamed Item, Nominal Lawvere theories: a category theoretic account of equational theories with names, Predicate calculus of arbitrarily high finite order, Functional Semantics, λ-definable functionals andβη conversion, Towards Lambda Calculus Order-Incompleteness, Representing Model Theory in a Type-Theoretical Logical Framework, Automath and Pure Type Systems, Formal SOS-Proofs for the Lambda-Calculus, Gate splitting in LOTOS specifications using abstract interpretation, Unnamed Item, European meeting of the Association for Symbolic Logic, Mons, Belgium, 1978, On the longest perpetual reductions in orthogonal expression reduction systems, On the proof theory of Coquand's calculus of constructions, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), Strongly Normalising Cut-Elimination with Strict Intersection Types, (In)efficiency and reasonable cost models, Constructive Recursive Functions, Church’s Thesis, and Brouwer’s Theory of the Creating Subject: Afterthoughts on a Parisian Joint Session, Proof-Theoretic Semantics and Feasibility, Completeness, invariance and λ-definability, Redexes are stable in the λ-calculus
