scientific article; zbMATH DE number 1042221

Publication date: 3 August 1997

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

intuitionistic logic functional programming language type-theory lambda-calculus type-checking algorithm type-assignment polymorphic theories

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

Practical Proof Search for Coq by Type Inhabitation, The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL, Coq formalization of the higher-order recursive path ordering, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Combinatory logic with polymorphic types, Extended First-Order Logic, Intuitionistic games: determinacy, completeness, and normalization, Hammer for Coq: automation for dependent type theory, The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic, A decidable theory of type assignment, Type Inference for Rank 2 Gradual Intersection Types, Unnamed Item, Type inference for rank-2 intersection types using set unification, An algebra of behavioural types, A (machine-oriented) logic based on pattern matching, Structural rules and algebraic properties of intersection types, Quantitative weak linearisation, On some enumerative problems in lambda calculus, On Polymorphic Recursion, Type Systems, and Abstract Interpretation, When are different type-logical semantic definitions defining equivalent meanings?, On the number of types, Counting and generating terms in the binary lambda calculus, An Investigation into Intuitionistic Logic with Identity, Grammar induction by unification of type-logical lexicons, Unnamed Item, A Higher-Order Calculus of Computational Fields, CARNAP’S DEFENSE OF IMPREDICATIVE DEFINITIONS, Unnamed Item, A typed lambda calculus with intersection types, A coinductive approach to proof search through typed lambda-calculi, Term-space semantics of typed lambda calculus, Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus, Kripke semantics for higher-order type theory applied to constraint logic programming languages, Studying provability in implicational intuitionistic logic, Abstract Families of Abstract Categorial Languages, Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, Polymorphic type inference for the relational algebra, Tachyon instability and Kondo type models, Learnability of type-logical grammars, Second-order abstract categorial grammars as hyperedge replacement grammars, On fuzzy type theory, Type system in programming languages, Semantic bootstrapping of type-logical grammar, Abstract deduction and inferential models for type theory, Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules, THE CONCEPTHORSEIS A CONCEPT, Counting proofs in propositional logic, Substitution contradiction, its resolution and the Church-Rosser theorem in TIL, Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete, Cut-free Gentzen calculus for multimodal CK, Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search, Weak linearization of the lambda calculus, Does the Implication Elimination Rule Need a Minor Premise?, Pre-grammars and inhabitation for a subset of rank 2 intersection types, A structural approach to reversible computation, KURT GÖDEL ON LOGICAL, THEOLOGICAL, AND PHYSICAL ANTINOMIES, Redexes are stable in the λ-calculus, A short note on type-inhabitation: formula-trees vs. game semantics, Why ramify?