scientific article

zbMath0642.03002MaRDI QIDQ4040149

Philip J. Scott

Publication date: 5 June 1993

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

zbMATH Keywords

Cartesian closed categoriestyped lambda calculusfree toposeshigher-order intuitionistic type theory

Mathematics Subject Classification ID

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 (39)

On concurrent games with payoff ⋮ A Finite Axiomatisation of Finite-State Automata Using String Diagrams ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Coherence in SMCCs and equivalences on derivations in IMML with unit ⋮ Universal profinite domains ⋮ Morita equivalence of semigroups revisited: firm semigroups ⋮ Partial morphisms in categories of effective objects ⋮ Is `no' a force-indicator? Yes, sooner or later! ⋮ Sheaf tools for computation ⋮ Transport of finiteness structures and applications ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ A formal logic for formal category theory ⋮ On the equational definition of the least prefixed point. ⋮ CHAD for expressive total languages ⋮ The syntactic side of autonomous categories enriched over generalised metric spaces ⋮ Linearizing Combinators ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A string diagrammatic axiomatisation of finite-state automata ⋮ Reverse AD at higher types: pure, principled and denotationally correct ⋮ CATEGORICAL COMPLEXITY ⋮ New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic ⋮ Comparing Hagino's categorical programming language and typed lambda- calculi ⋮ Type Similarity for the Lambek-Grishin Calculus Revisited ⋮ Partial Recursive Functions and Finality ⋮ Sets in homotopy type theory ⋮ Ehresmann semigroups from a range restriction viewpoint ⋮ Filter quotients and non-presentable \((\infty,1)\)-toposes ⋮ Unnamed Item ⋮ Topological rigidity as a monoidal equivalence ⋮ Unnamed Item ⋮ Notions of computation and monads ⋮ Curry-Howard-Lambek correspondence for intuitionistic belief ⋮ Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus ⋮ Dynamic game semantics ⋮ Unnamed Item ⋮ Geometry and generality in Frege's philosophy of arithmetic. ⋮ Automorphisms of types in certain type theories and representation of finite groups ⋮ Structuring co-constructive logic for proofs and refutations

This page was built for publication: