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 (only showing first 100 items - show all)
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
This page was built for publication:
