scientific article; zbMATH DE number 1042221
From MaRDI portal
Publication:4346206
functional programming languageintuitionistic logiclambda-calculuspolymorphic theoriestype-assignmenttype-checking algorithmtype-theory
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15)
Recommendations
Cited in
(66)- Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules
- Counting proofs in propositional logic
- Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete
- Hammer for Coq: automation for dependent type theory
- On the number of types
- Semantic bootstrapping of type-logical grammar
- Grammar induction by unification of type-logical lexicons
- Term-space semantics of typed lambda calculus
- Combinatory logic with polymorphic types
- On some enumerative problems in lambda calculus
- A coinductive approach to proof search through typed lambda-calculi
- Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
- Substitution contradiction, its resolution and the Church-Rosser theorem in TIL
- Pre-grammars and inhabitation for a subset of rank 2 intersection types
- A short note on type-inhabitation: formula-trees vs. game semantics
- Why ramify?
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
- Weak linearization of the lambda calculus
- A structural approach to reversible computation
- The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
- Game semantics and uniqueness of type inhabitance in the simply-typed -calculus
- Does the implication elimination rule need a minor premise?
- Extended First-Order Logic
- Intuitionistic games: determinacy, completeness, and normalization
- On Polymorphic Recursion, Type Systems, and Abstract Interpretation
- Simple Types in Type Theory: Deep and Shallow Encodings
- A decidable theory of type assignment
- An algebra of behavioural types
- When are different type-logical semantic definitions defining equivalent meanings?
- scientific article; zbMATH DE number 1497851 (Why is no real title available?)
- A higher-order calculus of computational fields
- Studying provability in implicational intuitionistic logic: the formula tree approach
- Abstract families of abstract categorial languages
- Learnability of type-logical grammars
- The concept \textit{horse} is a concept
- A unifying framework for type inhabitation
- Kurt Gödel on logical, theological, and physical antinomies
- scientific article; zbMATH DE number 7455712 (Why is no real title available?)
- Practical Proof Search for Coq by Type Inhabitation
- Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics
- Type Inference for Rank 2 Gradual Intersection Types
- An investigation into intuitionistic logic with identity
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Redexes are stable in the -calculus
- Counting and generating terms in the binary lambda calculus
- Carnap's defense of impredicative definitions
- Tachyon instability and Kondo type models
- Type system in programming languages
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
- Type inference for rank-2 intersection types using set unification
- A (machine-oriented) logic based on pattern matching
- Structural rules and algebraic properties of intersection types
- Quantitative weak linearisation
- Lemmas: generation, selection, application
- Context and the composition of meaning
- Comments on the contributions
- Investigations into proof structures
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Pregrammars and intersection types
- Polymorphic type inference for the relational algebra
- On fuzzy type theory
- Cut-free Gentzen calculus for multimodal CK
- Coq formalization of the higher-order recursive path ordering
- A typed lambda calculus with intersection types
- Second-order abstract categorial grammars as hyperedge replacement grammars
- Abstract deduction and inferential models for type theory
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 Q4346206)
