A collection of a bunch of interesting PL links and papers.**
- Propositions as Types
- Linear Types can change the world!
- Ur/Web: A Simple Model for Programming the Web
- Practical Affine Types
- Dependent Types for JavaScript
- Lazy Abstraction with Interpolants
- Adding Nesting Structure to Words
- Refinement Types for Haskell
- What Every Programmer Should Know About Memory
- Undefined Behavior: What Happened to My Code?
- Abstractions from Proofs
- Pycket: A Tracing JIT For a Functional Language
- Capabilities for Uniqueness and Borrowing
- Colored Local Type Inference
- Dual Intuitionistic Linear Logic
- A taste of linear logic
- Propositions as Sessions
- Lightweight Linear Types in System F◦
- Uniqueness Typing Simplified
- Fusion for Free Efficient Algebraic Effect Handlers
- Contracts for Higher-Order Functions
- Comparison of Erlang Runtime System and Java Virtual Machine
- System FC with Explicit Kind Equality
- Call-by-Value is Dual to Call-by-Name
- SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
- Out of the Tar Pit
- A Very Modal Model of a Modern, Major, General Type System
- From Sets to Types to Categories to Sets∗
- Burritos for the Hungry Mathematician
- Scalable Component Abstractions
- Is Sound Gradual Typing Dead?
- A Syntactic Theory of Dynamic Binding
- The Expression Problem, Trivially! (Short Paper)
- Stack Safety for Free
- Should I use a Monad or a Comonad?
- A Nanopass Framework for Compiler Education
- The Two Dualities of Computation: Negative and Fractional Types
- A Foundation for Embedded Languages
- First-Class Phantom Types
- Scrap your boilerplate with class: extensible generic functions
- A reflection on types
- The Emperor’s Old Clothes
- System F-omega with Equirecursive Types for Datatype-Generic Programming
- Type Classes as Objects and Implicits
- Haskell Is Not Not ML
- Functional Programming with Structured Graphs
- LifeJacket: Verifying precise floatingpoint optimizations in LLVM
- Notions of computation and monads
- Desugaring Haskell’s do-notation Into Applicative Operations
- Löb’s Theorem
- Just-in-Time Static Type Checking for Dynamic Languages
- Exceptional Continuations in JavaScript
- Java Generics are Turing Complete
- One VM to Rule Them All
- A tutorial on the universality and expressiveness of fold
- Sequent Calculus as a Compiler Intermediate Language
- What can the programming language Rust do for astrophysics?
- Covariance and Contravariance: a fresh look at an old issue
** Will add more with time.