Publication:3922646

No author found.

Publication date: 1980

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

01A70: Biographies, obituaries, personalia, bibliographies

03A05: Philosophical and critical aspects of logic and foundations

03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

03-06: Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations

18D15: Closed categories (closed monoidal and Cartesian closed categories, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

Fixed points and unfounded chains, On the expressive power of first-order boolean functions in PCF, On the longest perpetual reductions in orthogonal expression reduction systems, 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, Kripke-style models for typed lambda calculus, Extraction of redundancy-free programs from constructive natural deduction proofs, Weak typed Böhm theorem on IMLL, A category-theoretic characterization of functional completeness, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, Programs as proofs: A synopsis, Complexity of the combinator reduction machine, Needed reduction and spine strategies for the lambda calculus, Termination of rewriting, One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus, The calculus of constructions, 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, Generalization from partial parametrization in higher-order type theory, 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\), Type checking with universes, Finite type structures within combinatory algebras, Filter models with polymorphic types, Conditional rewriting logic as a unified model of concurrency, Complete restrictions of the intersection type discipline, Constructing type systems over an operational semantics, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, From constructivism to computer science, Termination of permutative conversions in intuitionistic Gentzen calculi, Perpetual reductions in \(\lambda\)-calculus, Typing untyped \(\lambda\)-terms, or reducibility strikes again!, 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, Proofs as processes, Labelled domains and automata with concurrency, Label-selective \(\lambda\)-calculus syntax and confluence, On reduction-based process semantics, Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus, Strong normalization from weak normalization in typed \(\lambda\)-calculi, Full abstraction for the second order subset of an Algol-like language, Embedding of a free cartesian-closed category into the category of sets, New Curry-Howard terms for full linear logic, Revisiting the notion of function, Coherence for sharing proof-nets, Chu spaces as a semantic bridge between linear logic and mathematics., A linear logical framework, Behavioural inverse limit \(\lambda\)-models, Reduction of finite and infinite derivations, Proof nets, garbage, and computations, Relating conflict-free stable transition and event models via redex families, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Typing and computational properties of lambda expressions, The foundation of a generic theorem prover, Extraction and verification of programs by analysis of formal proofs, Equality between functionals in the presence of coproducts, The combinator S, Perpetuality and uniform normalization in orthogonal rewrite systems, Reducibility between classes of port graph grammar., MELL in the calculus of structures, Principality and type inference for intersection types using expansion variables, Intersection types for explicit substitutions, Projecting sequential algorithms on strongly stable functions, Easiness in graph models, The HASCASL prologue: Categorical syntax and semantics of the partial \(\lambda\)-calculus, Ensuring termination by typability, Logic of subtyping, The conflict-free reduction geometry, Precomplete Equivalence Relations in Dominical Categories