scientific article

No author found.

Publication date: 1980

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

domains normalization reductions semantics abstraction syntax typed lambda calculus reflexive domains typed terms illative combinatory logic combinatorial algebras automath biography and complete bibliography of H. B. Curry Curry's program extensions of combinatory logic formulae-as-types notion models of lambda-calculus type-free theories

Mathematics Subject Classification ID

Biographies, obituaries, personalia, bibliographies (01A70) Philosophical and critical aspects of logic and foundations (03A05) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items

Reducibility between classes of port graph grammar. ⋮ Proofs, grounds and empty functions: epistemic compulsion in Prawitz's semantics ⋮ Logical relations and parametricity -- a Reynolds programme for category theory and programming languages ⋮ Graph easy sets of mute lambda terms ⋮ Easiness in graph models ⋮ The HASCASL prologue: Categorical syntax and semantics of the partial \(\lambda\)-calculus ⋮ MELL in the calculus of structures ⋮ Principality and type inference for intersection types using expansion variables ⋮ Intersection types for explicit substitutions ⋮ Proofs as processes ⋮ Labelled domains and automata with concurrency ⋮ Needed reduction and spine strategies for the lambda calculus ⋮ Label-selective \(\lambda\)-calculus syntax and confluence ⋮ On reduction-based process semantics ⋮ Termination of rewriting ⋮ Partial combinatory algebra and generalized numberings ⋮ Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus ⋮ The calculus of constructions ⋮ Full abstraction for the second order subset of an Algol-like language ⋮ Weak typed Böhm theorem on IMLL ⋮ An intersection problem for finite automata ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Projecting sequential algorithms on strongly stable functions ⋮ Generalization from partial parametrization in higher-order type theory ⋮ Embedding of a free cartesian-closed category into the category of sets ⋮ On a conjecture of Bergstra and Tucker ⋮ Concurrency and atomicity ⋮ A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\) ⋮ Rewriting Strategies and Strategic Rewrite Programs ⋮ New Curry-Howard terms for full linear logic ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ In the Search of a Naive Type Theory ⋮ Revisiting the notion of function ⋮ Coherence for sharing proof-nets ⋮ Chu spaces as a semantic bridge between linear logic and mathematics. ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ A linear logical framework ⋮ Jumps of computably enumerable equivalence relations ⋮ A category-theoretic characterization of functional completeness ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ Towards the range property for the lambda theory \(\mathcal H\) ⋮ On strong normalization and type inference in the intersection type discipline ⋮ A typed lambda calculus with intersection types ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Type checking with universes ⋮ Decidability of bounded higher-order unification ⋮ Finite type structures within combinatory algebras ⋮ Filter models with polymorphic types ⋮ Uniqueness of Scott's reflexive domain in \(P\omega \) ⋮ Recognizable languages in concurrency monoids ⋮ A characterization of lambda definability in categorical models of implicit polymorphism ⋮ Conditional rewriting logic as a unified model of concurrency ⋮ Complete restrictions of the intersection type discipline ⋮ Constructing type systems over an operational semantics ⋮ A domain model characterising strong normalisation ⋮ Preface to the special volume ⋮ Cryptographic logical relations ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Evaluating lambda terms with traversals ⋮ On computably enumerable structures ⋮ Ensuring termination by typability ⋮ Logic of subtyping ⋮ Precomplete numberings ⋮ Fixed point theorems for precomplete numberings ⋮ Typing and computational properties of lambda expressions ⋮ From constructivism to computer science ⋮ Termination of permutative conversions in intuitionistic Gentzen calculi ⋮ Studying Operational Models of Relaxed Concurrency ⋮ The foundation of a generic theorem prover ⋮ Extraction and verification of programs by analysis of formal proofs ⋮ Perpetual reductions in \(\lambda\)-calculus ⋮ Simple Easy Terms ⋮ Reducibility ⋮ Reduction of finite and infinite derivations ⋮ The noneffectivity of Arslanov's completeness criterion and related theorems ⋮ Strong normalization property for second order linear logic ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again! ⋮ Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms ⋮ Programs as proofs: A synopsis ⋮ Proof nets, garbage, and computations ⋮ Equality between functionals in the presence of coproducts ⋮ The combinator S ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ The conflict-free reduction geometry ⋮ A Framework for Defining Logical Frameworks ⋮ Kripke-style models for typed lambda calculus ⋮ Constructive proofs of the range property in lambda calculus ⋮ Combinatory reduction systems: Introduction and survey ⋮ Set-theoretical and other elementary models of the \(\lambda\)-calculus ⋮ Some examples of non-existent combinators ⋮ Extraction of redundancy-free programs from constructive natural deduction proofs ⋮ Complete Laziness: a Natural Semantics ⋮ Minimality in a Linear Calculus with Iteration ⋮ Relating conflict-free stable transition and event models via redex families ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic ⋮ Effective inseparability and its applications ⋮ Complexity of the combinator reduction machine ⋮ THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS) ⋮ Optimal normalization in orthogonal term rewriting systems ⋮ Relating two categorical models of term rewriting ⋮ Computational logic: its origins and applications ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Fixpoints and relative precompleteness ⋮ The geometry of orthogonal reduction spaces ⋮ Intuitive counterexamples for constructive fallacies ⋮ Formal categorical reasoning ⋮ A user's friendly syntax to define recursive functions as typed λ-terms ⋮ Conservativity between logics and typed λ calculi ⋮ Developing certified programs in the system Coq the program tactic ⋮ Extremal numberings and fixed point theorems ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Types, abstraction, and parametric polymorphism, part 2 ⋮ From domains to automata with concurrency ⋮ A kleene theorem for recognizable languages over concurrency monoids ⋮ Two different strong normalization proofs? ⋮ GENERALIZATIONS OF THE RECURSION THEOREM ⋮ Peirce's Rule in a Full Natural Deduction System ⋮ Automath and Pure Type Systems ⋮ Fixed points and unfounded chains ⋮ Precomplete Equivalence Relations in Dominical Categories ⋮ On the expressive power of first-order boolean functions in PCF ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Truth and Proof in Intuitionism ⋮ Type Theory and Homotopy ⋮ Aspects of Categorical Recursion Theory ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations ⋮ Redexes are stable in the λ-calculus ⋮ Classical lambda calculus in modern dress ⋮ Computable embeddability for algebraic structures ⋮ Relative normalization in Deterministic Residual Structures ⋮ Effective longest and infinite reduction paths in untyped λ-calculi