scientific article; zbMATH DE number 3735770
From MaRDI portal
Publication:3922646
abstractionautomathbiography and complete bibliography of H. B. Currycombinatorial algebrasCurry's programdomainsextensions of combinatory logicformulae-as-types notionillative combinatory logicmodels of lambda-calculusnormalizationreductionsreflexive domainssemanticssyntaxtype-free theoriestyped lambda calculustyped terms
Biographies, obituaries, personalia, bibliographies (01A70) 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) Philosophical and critical aspects of logic and foundations (03A05) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)
Cited in
(only showing first 100 items - show all)- Strong normalization property for second order linear logic
- 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 - 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 -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 -calculus syntax and confluence
- On reduction-based process semantics
- Kripke models and the (in)equational logic of the second-order -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 -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
- Jumps of computably enumerable equivalence relations
- 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
- Evaluating lambda terms with traversals
- Precomplete numberings
- Effective inseparability and its applications
- Proofs, grounds and empty functions: epistemic compulsion in Prawitz's semantics
- Partial combinatory algebra and generalized numberings
- On computably enumerable structures
- Fixed point theorems for precomplete numberings
- Easiness in graph models
- The HASCASL prologue: Categorical syntax and semantics of the partial \(\lambda\)-calculus
- Decidability of bounded higher-order unification
- Cryptographic logical relations
- Ensuring termination by typability
- Logic of subtyping
- The conflict-free reduction geometry
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Studying Operational Models of Relaxed Concurrency
- Simple easy terms
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- A framework for defining logical frameworks
- Complete laziness: a natural semantics
- Minimality in a linear calculus with iteration
- Graph easy sets of mute lambda terms
- Rewriting strategies and strategic rewrite programs
- Characterising Strongly Normalising Intuitionistic Sequent Terms
- In the Search of a Naive Type Theory
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Precomplete Equivalence Relations in Dominical Categories
- Computational logic: its origins and applications
- A resource aware semantics for a focused intuitionistic calculus
- The geometry of orthogonal reduction spaces
- From domains to automata with concurrency
- A Kleene theorem for recognizable languages over concurrency monoids
- Two \textit{different} strong normalization proofs?
- GENERALIZATIONS OF THE RECURSION THEOREM
- Automath and Pure Type Systems
- Aspects of categorical recursion theory
- Optimal normalization in orthogonal term rewriting systems
- Relating two categorical models of term rewriting
- Fixpoints and relative precompleteness
- Intuitive counterexamples for constructive fallacies
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3922646)
