Pregrammars and intersection types

DOI10.4230/LIPICS.CSL.2021.14MaRDI QIDQ6839824zbMATH OpenFDO

Authors Sabine Broda

Publication date 23 March 2026

Copyright license Creative Commons Attribution 3.0 Unported

zbMATH Keywords

inhabitationintersection typespregrammars

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 2185668 (Why is no real title available?)
• scientific article; zbMATH DE number 2185726 (Why is no real title available?)
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 1342274 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1956517 (Why is no real title available?)
• scientific article; zbMATH DE number 1984520 (Why is no real title available?)
• A Datalog recognizer for almost affine \(\lambda \)-CFGs
• A new type assignment for λ-terms
• A unifying framework for type inhabitation
• An extension of basic functionality theory for -calculus
• Elaborating intersection and union types
• Exact flow analysis
• Example-directed synthesis: a type-theoretic interpretation
• From polyvariant flow information to intersection and union types
• Functional Characters of Solvable Terms
• Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete
• Inhabitation for non-idempotent intersection types
• Inhabitation of Low-Rank Intersection Types
• Intersection type calculi of bounded dimension
• Intuitionistic propositional logic is polynomial-space complete
• Loader and Urzyczyn are logically related
• Non-idempotent intersection types for the lambda-calculus
• Normal proofs and their grammar
• Pre-grammars and inhabitation for a subset of rank 2 intersection types
• Recognizability in the Simply Typed Lambda-Calculus
• Staged composition synthesis
• Strict intersection types for the lambda calculus
• The Complexity of Inhabitation with Explicit Intersection
• The Inhabitation Problem for Rank Two Intersection Types
• The emptiness problem for intersection types
• Typability in bounded dimension
• Uniqueness of normal proofs in implicational intuitionistic logic

This page was built for publication: Pregrammars and intersection types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6839824)