Research and Reading
Bookmarks
Polarized Subtyping
Classics
- Types are not sets
- Type systems
- The definition of standard ML (revised)
- Types and programming languages
- The situation in logic
- Deforestation, program transformation, and cut-elimination
On Types
- Maybe not 🎥
- Local type inference
- Counterexamples in type systems - counterexamples in type systems
- Preliminary design of the programming language Forsythe
- Design of the programming language FORSYTHE
- Nested datatypes
Call-by-Push-Value
- Call-by-push-value 📜
- Call-by-push-value - A subsuming paradigm
- Effects and coeffects in call-by-push-value (extended version)
- Call-by-push-value_ Decomposing call-by-value and call-by-name
- Extended call-by-push-value - Reasoning about effectful programs and evaluation order
- Probabilistic call by push value
- I'm betting on call-by-push-value · thunderseethe's devlog 💻
- Adjunction models for call-by-push-value with stacks
- Intersection types for a strong call-by-push value - normalisations and solvability
- Semantic domain_ Focusing is not call-by-push-value 💻
- The fire triangle_ how to mix substitution, dependent elimination, and effects
Sub(typing)
- Inheritance is subtyping
- Subtyping recursive types
- Programming with intersection types and bounded polymorphism
- Iowa type theory commute_ Subtyping, the golden key
- Revisiting iso-recursive subtyping
- Coinductive axiomatization of recursive type equality and subtyping
- Subtyping, declaratively
- On the preciseness of subtyping in session types
- Subtyping for session types in the pi-Calculus
- Polarized higher-order subtyping
- Algebraic subtyping_ Distinguished dissertation 2017 📜
- The simple essence of algebraic subtyping_ principal type inference with subtyping made easy (functional pearl)
- A mechanical soundness proof for subtyping over recursive types
- Subtyping by folding an inductive relation into a coinductive one
- Practical subtyping for Curry-Style languages
- Subtyping union types
- Efficient recursive subtyping
- Recursive subtyping for all
Theory
- Sequent calculi for induction and infinite descent
- Polarised intermediate representation of lambda calculus with sums
- The logical basis of evaluation order and pattern-matching
- Introduction and elimination, left and right
- Search for program structure
- On the unity of duality
- A unified system of type refinements 📜
- Polarity in type theory _ existential type 💻
- A logical framework with higher-order rational (circular) terms
- Monadic compiler calculation (functional pearl)
- Positive recursive type assignment
- Syntax and Models of a non-Associative Composition of Programs and Proofs. (Syntaxe et modèles d'une composition non-associative des programmes et des preuves)
- Principal type-schemes for functional programs
- Principal type schemes for an extended type theory
- A type assignment for the strongly normalizable lambda-terms
- A filter lambda model and the completeness of type assignment
- Adjoint logic
- Linear logic, monads and the lambda calculus
- Direct models of the computational lambda-calculus
- Signals and comonads
- Integrating induction and coinduction via closure operators and proof cycles
- Structural induction and coinduction in a fibrational setting
- Resumptions, weak bisimilarity and big-step semantics for while with interactive I_O_ An exercise in mixed induction-coinduction
- On the semantics of fair parallelism
- L'arithmetique fonctionnelle du second ordre avec points fixes
- Monadic compiler calculation (functional pearl)
- Bisimulation as path type for guarded recursive types
- Will deflation lead to depletion_ On non-monotone fixed point inductions
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- On the logical strength of confluence and normalisation for cyclic proofs
Intersection Types & Union Types
- Monadic intersection types, relationally
- Intersection types and computational effects
- A tale of intersection types
- Programming with union, intersection, and negation types
- The duality of classical intersection and union types
- Intersection and union types - Syntax and semantics
- Hybrid intersection types for PCF (extended version)
- Type assignment for intersections and unions in call-by-value languages
- The coherence of languages with intersection types
- A new type assignment for λ-terms
- Taming the merge operator
- Elaborating intersection and union types
- Disjoint intersection types
- Distributing intersection and union types with splits and duality (functional pearl)
- Resolution as intersection subtyping via Modus Ponens
- Tridirectional typechecking
- Union types with disjoint switches
- Empowering union and intersection types with integrated subtyping
- A blend of intersection types and union types 📜
- Subtyping and intersection types revisited
- On subtyping-relation completeness, with an application to iso-recursive types
- An extension of the basic functionality theory for the λ-calculus
Refinement Types
- Refinement types for ML
- Contextual refinement types
- Refinement kinds - type-safe programming with practical type-level computation
- Type refinements in an open world (extended abstract)
- Structural refinement types
- Practical refinement-type checking
- Refinement types and computational duality
- Refinement types for haskell
- Extensible datasort refinements
- Explicit refinement types
- Focusing on refinement typing
- A refinement type by any other name _ weaselhat 💻
- LiquidHaskell_ experience with refinement types in the real world
- Refined typechecking with Stardust
- Total correctness type refinements for communicating processes
Focusing
Record Operations and Concatenation
- A calculus with recursive types, record concatenation and subtyping
- Operations on records
- A record calculus based on symmetric concatenation
- Extensible records in a pure calculus of subtyping
- Complete type inference for simple objects
- A new modular implementation for stateful traits
Type Difference
Semantic Typing & Step Indexing
- Step-indexed syntactic logical relations for recursive and quantified types
- Semantics of types for mutable state 📜
- Transfinite step-indexing for termination
- An indexed model of recursive types for foundational proof-carrying code
- Logical step-indexed logical relations
- What type soundness theorem do you really want to prove_ 💻
- RustBelt_ securing the foundations of the rust programming language
Semantic Subtyping
- Covariance and Controvariance_ a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)
- A gentle introduction to semantic subtyping
- Set-theoretic types for polymorphic variants
- Semantic subtyping
- Semantic subtyping_ Dealing set-theoretically with function, union, intersection, and negation types
- Semantic subtyping for non-strict languages
- On the semantic expressiveness of recursive types
- Polymorphic functions with set-theoretic types_ part 1_ syntax, semantics, and evaluation
- Polymorphic functions with set-theoretic types_ Part 2_ Local type inference and type reconstruction
- Polymorphic set-theoretic types for functional languages. (Types ensemblistes polymorphes pour les langages fonctionnels)
Polymorphism
- Parametric subtyping for structural parametric polymorphism
- Types, abstraction and parametric polymorphism
- Simple type inference for structural polymorphism
- Getting F-bounded polymorphism into shape
- F-bounded polymorphism for object-oriented programming
- Structural subtyping as parametric polymorphism
- An ideal model for recursive polymorphic types
Bidirectional Typing
- Bidirectional typing
- Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
Gradual Typing
- Hack_ a new programming language for HHVM - engineering at meta
- Gradual typing from theory to practice _ SIGPLAN blog 💻
- TypeScript playground - soundness
- TypeScript_ Documentation - type compatibility
- Type-checking unsoundness - standardize treatment of such issues among TypeScript - Issue 9825
- Gradual type theory
- Gradual typing as if types mattered
- Sound gradual typing_ only mostly dead
- Is sound gradual typing dead_
- Sums of uncertainty_ refinements go gradual
Compositional Programming
- Direct foundations for compositional programming
- Imperative compositional programming
- A bowtie for a beast_ Overloading, eta expansion, and extensible data types
Sized Types
- Polarized subtyping for sized types
- Well-founded recursion with copatterns and sized types[
- Wellfounded recursion with copatterns_ A unified approach to termination and productivity
- Mixed Inductive_Coinductive types and strong normalization
- Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
Dependent Types
Session Types
- Nested session types
- Linear type theory for asynchronous session types
- Syntactic considerations on recursive types
- Machine-checked semantic session typing