Polarized subtyping
From MaRDI portal
Publication:6166799
DOI10.1007/978-3-030-99336-8_16zbMath1528.68082arXiv2201.10998OpenAlexW4226343274MaRDI QIDQ6166799
Zeeshan Lakhani, Henry DeYoung, Frank Pfenning, Ankush Das, Andreia Mordido
Publication date: 3 August 2023
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2201.10998
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Call-by-push-value: Decomposing call-by-value and call-by-name
- A theory of type polymorphism in programming
- Structural induction and coinduction in a fibrational setting
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- Integrating induction and coinduction via closure operators and proof cycles
- Nested session types
- Subtyping for session types in the pi calculus
- Practical Foundations for Programming Languages
- Polymorphic Functions with Set-Theoretic Types
- Intersection types and computational effects
- Recursive subtyping revealed
- Set-theoretic types for polymorphic variants
- Sequent calculi for induction and infinite descent
- Polarized Subtyping for Sized Types
- Semantic subtyping
- Tridirectional typechecking
- Mixed Inductive/Coinductive Types and Strong Normalization
- Positive recursive type assignment
- Subtyping, Declaratively
- Deforestation, program transformation, and cut-elimination
- Linear type theory for asynchronous session types
- Wellfounded recursion with copatterns
- Sums of uncertainty: refinements go gradual
- Well-founded recursion with copatterns and sized types
- Polymorphic functions with set-theoretic types
- Automata, Languages and Programming
- Programming Languages and Systems
This page was built for publication: Polarized subtyping
