scientific article
From MaRDI portal
Publication:3727946
zbMath0596.03002MaRDI QIDQ3727946
Joachim Lambek, Philip J. Scott
Publication date: 1986
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40) Research exposition (monographs, survey articles) pertaining to category theory (18-02) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to category theory (18-01) Foundations, relations to logic and deductive systems (18A15)
Related Items
A categorical formulation for critical-pair/completion procedures, Initial algebra semantics for lambda calculi, Semantic analysis of normalisation by evaluation for typed lambda calculus, A categorical interpretation of Landin's correspondence principle, Constructive set theoretic models of typed combinatory logic, Unnamed Item, Unnamed Item, Coherence for bicategorical cartesian closed structure, Adhesive and quasiadhesive categories, A matching process modulo a theory of categorical products, An extension of system F with subtyping, Dictoses, Declarative continuations: An investigation of duality in programming language semantics, Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory, The Relation Between Logic, Set Theory and Topos Theory as it Is Used by Alain Badiou, From gs-monoidal to oplax cartesian categories: constructions and functorial completeness, The Deduction Theorem (Before and After Herbrand), Choice and independence of premise rules in intuitionistic set theory, Categorical models of the differential λ-calculus, A general framework for the semantics of type theory, Protocol choice and iteration for the free cornering, Structured handling of scoped effects, Types, abstraction, and parametric polymorphism, part 2, Reversible monadic computing, Healthiness conditions for predicate transformers, Monoidal logics: completeness and classical systems, Unnamed Item, Intuitionistic sets and ordinals, Deductive Completeness, Cofree coalgebras and differential linear logic, A logical framework combining model and proof theory, Fuzzy logic and enriched categories, A Logical Basis for Quantum Evolution and Entanglement, Multi-Sorted Residuation, Chasing Diagrams in Cryptography, Structures of systems 1. Cohomology of manufacturing and supply network-like systems, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, REPRESENTING CONJUNCTIVE DEDUCTIONS BY DISJUNCTIVE DEDUCTIONS, On the role of description, On the semantics of classical disjunction, Subtractive logic, Introduction to Type Theory, Proof theory in the abstract, Two applications of analytic functors, Free \(\mu\)-lattices, Unnamed Item, Why Sets?, A proposed categorical semantics for Pure ML, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, CONSTRUCTIVE REFLECTIVITY PRINCIPLES FOR REGULAR THEORIES, Inferential Semantics, Monoidal-closed categories of tree automata, Pointers in Recursion: Exploring the Tropics, ETA-RULES IN MARTIN-LÖF TYPE THEORY, A topos foundation for theories of physics: I. Formal languages for physics, Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory, Constructive Modalities with Provability Smack, Probabilistic Completion of Nondeterministic Models, Classical lambda calculus in modern dress, Nominal lambda calculus: an internal language for FM-Cartesian closed categories, Towards a notion of lambda monoid, Category theory, logic and formal linguistics: some connections, old and new, On the implementation of abstract data types by programming language constructs, Logical systems. I: Internal calculi., Kleene computable functionals and the higher order existence property, The linear abstract machine, Algebra of constructions. I. The word problem for partial algebras, Semantics of higher-order quantum computation via geometry of interaction, A model for spacetime: the role of interpretation in some Grothendieck topoi, Causal categories: relativistically interacting processes, A categorical semantics for polarized MALL, Partial Horn logic and Cartesian categories, Toposes and intuitionistic theories of types, E-ccc: Between ccc and topos, Unique normal forms for lambda calculus with surjective pairing, What is the world of mathematics?, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Natural deduction and coherence for weakly distributive categories, Finitary topos for locally finite, causal and quantal vacuum Einstein gravity, Internal diagrams and archetypal reasoning in category theory, A reduction theorem for the Kripke-Joyal semantics: forcing over an arbitrary category can always be replaced by forcing over a complete Heyting algebra, Quotient completion for the foundation of constructive mathematics, Monoidal computer. I: Basic computability by string diagrams, Syntax and semantics of the logic \({\mathcal L}_{\omega\omega}^\lambda\), Relating first-order set theories, toposes and categories of classes, Systems analysis of life cycle of large-scale information-control systems, Basic subtoposes of the effective topos, Modeling linear logic with implicit functions, Monad transformers as monoid transformers, Categorical approaches to non-commutative fuzzy logic, The Peirce translation, Monoidal indeterminates and categories of possible worlds, Using formal methods with SysML in aerospace design and engineering, Codatatypes in ML, E-ccc: between ccc and topos, - its expressive power from the viewpoint of data type theory, Do-it-yourself type theory, A category-theoretic characterization of functional completeness, Semantical analysis of specification logic, A note on Russell's paradox in locally Cartesian closed categories, Pluri-adjoints and preservation of finite limits, A generalization of the concept of sketch, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, On some connections between logic and category theory, Monoidal categories with natural numbers object, An induction principle for consequence in arithmetic universes, Linearity and iterator types for Gödel's system \(\mathcal T\), The categorical imperative: category theory as a foundation for deontic logic, Domain theory in logical form, Triposes, q-toposes and toposes, Modes of adjointness, Capture-avoiding substitution as a nominal algebra, Fixed-point operations on ccc's. I, Principles of programming with complex objects and collection types, A characterization of lambda definability in categorical models of implicit polymorphism, Equational abstractions, The seven virtues of simple type theory, Coherence and strictification for self-similarity, Equational theories for inductive types, Proving semantical equivalence of data specifications, Categories for computation in context and unified logic, Agnostic hyperintensional semantics, Prior's tonk, notions of logic, and levels of inconsistency: vindicating the pluralistic unity of science in the light of categorical logical positivism, A single complete rule for data refinement, Tail recursion through universal invariants, I-categories as a framework for solving domain equations, Linear logic, coherence and dinaturality, Functional interpretations of feasibly constructive arithmetic, Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category, Aspects of predicative algebraic set theory. I: Exact completion, Machine semantics, The identity type weak factorisation system, Gödel's system \(\mathcal T\) revisited, A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms, Defining effectiveness using finite sets. A study on computability, A higher-order theory of presupposition, How to be a structuralist all the way down, The proof monad, Categorical relationships between Goguen sets and ``two-sided categorical models of linear logic, Languages for monoidal categories, Saturated models in institutions, Introduction to Turing categories, Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness, Toward discourse representation via pregroup grammars, HasCasl: integrated higher-order specification and program development, Topos-theoretic extension of a modal interpretation of quantum mechanics, A note on inconsistencies caused by fixpoints in a cartesian closed category, Categorical and algebraic aspects of Martin-Löf type theory, List-arithmetic distributive categories: Locoi, Fixed points in Cartesian closed categories, Functorial polymorphism, Pushout-complements and basic concepts of grammars in toposes, On the algebraic structure of declarative programming languages, The structure of free closed categories, Manufacturing a Cartesian closed category with exactly two objects out of a C-monoid, An abstract framework for environment machines, Kripke-style models for typed lambda calculus, Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus, Regular algebra applied to language problems, An exactification of the monoid of primitive recursive functions, Termination and confluence in infinitary term rewriting, Generality of proofs and its Brauerian representation, Topological completeness for higher-order logic, Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model, The Logic of Bunched Implications, A combinatory account of internal structure, Cubical methods in homotopy type theory and univalent foundations, Some lambda calculi with categorical sums and products, Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type, Cartesian Monoids, Categorical fixed point calculus, Categorical reconstruction of a reduction free normalization proof, Decomposing typed lambda calculus into a couple of categorical programming languages, V-comprehensions and P space, HOL Light: An Overview, Least fixpoints of endofunctors of cartesian closed categories, The theory of semi-functors, Comprehending monads, Categorical models for non-extensional λ-calculi and combinatory logic, Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs, Unnamed Item, SIMILARITY LOGIC AND TRANSLATIONS, A model for syntactic control of interference, Coherence of subsumption, minimum typing and type-checking in F ≤, A new constructive logic: classic logic, Girard quantaloids, Lambek's categorical proof theory and Läuchli's abstract realizability, Meeting of the Association for Symbolic Logic, Chicago, 1989, Transport of finiteness structures and applications, Execution time of λ-terms via denotational semantics and intersection types, Provable isomorphisms of types, Compositional characterization of observable program properties, A remark on the theory of semi-functors, A comparison between monoidal and substructural logics, The virtues of eta-expansion, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Primitive recursion, equality, and a universal set, Simulating expansions without expansions, Interpreting Localized Computational Effects Using Operators of Higher Type, The glueing construction and lax limits, Categorical semantics for higher order polymorphic lambda calculus, Universality of Logic, Unnamed Item, Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness, Relating First-Order Set Theories and Elementary Toposes, Sound and complete axiomatisations of call-by-value control operators, Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi, A categorical approach to the semantics of argumentation, Hopf algebras and linear logic, A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators, Call-by-name Gradual Type Theory, On the unification problem for Cartesian closed categories, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, A confluent reduction for the λ-calculus with surjective pairing and terminal object, Can a Quantum Computer Run the von Neumann Architecture?, Unnamed Item, Unnamed Item, Unnamed Item, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, CANONICITY RESULTS OF SUBSTRUCTURAL AND LATTICE-BASED LOGICS, Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic, Selection functions, bar recursion and backward induction, Some reasons for generalising domain theory, Reflection principles for synthetic theories of smooth manifolds, Unnamed Item, Identity of Proofs Based on Normalization and Generality, An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras, CATEGORICAL FOUNDATIONS OF MATHEMATICS OR HOW TO PROVIDE FOUNDATIONS FORABSTRACTMATHEMATICS, Presheaf Models of Quantum Computation: An Outline, Using transformations in the implementation of higher-order functions, Type inference with simple subtypes, Unnamed Item, Unnamed Item, Unnamed Item, A Brief Introduction to Algebraic Set Theory, On geometry of interaction for polarized linear logic, Triangular Logic of Partial Toposes, Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?, On traced monoidal closed categories, Completeness and Categoricity, Part II: Twentieth-Century Metalogic to Twenty-first-Century Semantics, A categorical manifesto, Reflexive objects in topological categories, Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types, Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x ofT], Unnamed Item, From parametric polymorphism to models of polymorphic FPC, Supra-logic: using transfinite type theory with type variables for paraconsistency, Unnamed Item, The nominal/FM Yoneda Lemma, Characterizations of semantic domains for randomized algorithms, Unnamed Item, Abstract Beth definability in institutions, Unnamed Item, The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics, Extensions of Lambek Calculi, Categories with Families: Unityped, Simply Typed, and Dependently Typed, Aspects of Categorical Recursion Theory, Pomset Logic, FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION, Unnamed Item, Infinite populations, choice and determinacy, Interpolation property for bicartesian closed categories, The HASCASL prologue: Categorical syntax and semantics of the partial \(\lambda\)-calculus, Adapting innocent game models for the Böhm tree \(\lambda\)-theory, Paracategories. I: Internal paracategories and saturated partial algebras, Paracategories. II: Adjunctions, fibrations and examples from probabilistic automata theory, From global to local state, coalgebraically and compositionally, Computational adequacy for recursive types in models of intuitionistic set theory, Modality via iterated enrichment, A simplicial foundation for differential and sector forms in tangent categories, Ultraproducts and possible worlds semantics in institutions, Factor theory and the unity of opposites, A model for intuitionistic non-standard arithmetic, Stable power domains, Categorical abstract machines for higher-order typed \(\lambda\)-calculi, New-from-old full dualities via axiomatisation, Logic in Category Theory, GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY, On the semantics of the universal quantifier, Linear Läuchli semantics, Projecting sequential algorithms on strongly stable functions, A reduction rule for Peirce formula, Embedding of a free cartesian-closed category into the category of sets, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, On fixpoint objects and gluing constructions, Extending Lambek grammars to basic categorial grammars, Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator, On fixed-point theorems in synthetic computability, Liminf convergence in \(\Omega\)-categories, What is a logic translation?, Canonicity and normalization for dependent type theory, Chu spaces as a semantic bridge between linear logic and mathematics., A new framework for declarative programming, G-dinaturality., A fully abstract model for the \(\pi\)-calculus., Partially traced categories, Term rewriting for normalization by evaluation., Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Sheaf representation of monoidal categories, Relative full completeness for bicategorical Cartesian closed structure, Semantics of \textsc{OpenMath} and \textsc{MathML3}, Polyadic spaces and profinite monoids, Induction-recursion and initial algebras., An abstract cell model that describes the self-organization of cell function in living systems, Proper/residually-finite idempotent semirings., A survey of fuzzy set and topos theory, Continuations in possible-world semantics, Composition of deductions within the propositions-as-types paradigm, Quantitative domains and infinitary algebras, A semantic hierarchy for intuitionistic logic, Categorical models of the differential \(\lambda\)-calculus revisited, Categories with finite limits and stable binary coproducts can be subdirectly decomposed, Categorical models of polymorphism, Modal translations in substructural logics, System BV is NP-complete, On the structure of paradoxes, Cryptographic logical relations, Principal types of BCK-lambda-terms, Quantum number theory, A categorical semantics for fuzzy predicate logic, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Relating categorical semantics for intuitionistic linear logic, Functional models of neurobiological processes, Robust and ubiquitous on-off intermittency in active coupling, Syntactic forcing models for coherent logic, Combinatorial topology and constructive mathematics, Higher-order quantifier elimination, counter simulations and fault-tolerant systems, Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract), Monoidal Indeterminates and Categories of Possible Worlds, The semantic view of theories and higher-order languages, On sheaf cohomology and natural expansions, Structural induction and coinduction in a fibrational setting, Cartesian categories with natural numbers object, The foundation of a generic theorem prover, The free category with products on a multigraph, Possible worlds and resources: The semantics of \(\mathbf{BI}\), \(U\)-Sets as a possibilistic set theory, A Category-Theoretic Approach to Social Network Analysis, Proof-search in type-theoretic languages: An introduction, GS·Λ Theories, Adjunction Models For Call-By-Push-Value With Stacks, Classifying categories for partial equational logic, Safe recursion with higher types and BCK-algebra, Wellfounded trees in categories, The three arrows of Zeno. Cantorian and non-Cantorian concepts of the continuum and of motion, Topology, domain theory and theoretical computer science, Dinatural numbers, Formalizing abstract computability: Turing categories in Coq, A categorical critical-pair completion algorithm, An equational variant of Lawvere's natural numbers object, A short note on coherence and self-similarity, Order-enriched categorical models of the classical sequent calculus, A relative PCF-definability result for strongly stable functions and some corollaries, Equality between functionals in the presence of coproducts, A Local Graph-rewriting System for Deciding Equality in Sum-product Theories, The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus, Categories with sums and right distributive tensor product, Information categories, An internal language for autonomous categories, Are the traditional philosophies of mathematics really incompatible?
