scientific article; zbMATH DE number 1042221
From MaRDI portal
Publication:4346206
zbMath0906.03012MaRDI QIDQ4346206
Publication date: 3 August 1997
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
intuitionistic logicfunctional programming languagetype-theorylambda-calculustype-checking algorithmtype-assignmentpolymorphic theories
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 (64)
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 ⋮ Lemmas: generation, selection, application ⋮ Context and the composition of meaning ⋮ Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules ⋮ Comments on the contributions ⋮ THE CONCEPTHORSEIS A CONCEPT ⋮ Investigations into proof structures ⋮ 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?
This page was built for publication:
