Semantic Domain

On his blog, Bob Harper asks what, if anything, a declarative language is . He notes that "declarative" is often used to mean ...

My paper with Derek Dreyer, Internalizing Relational Parametricity in the Extensional Calculus of Constructions , has been accepted to CSL 2...

All three of the papers my coauthors and I submitted this year were accepted! Complete and Easy Bidirectional Typechecking for Higher-Ra...

Proof theorists often observe that linear logic is like regular logic, only everything works better . In this post, I'll give a very st...

Yesterday, John Reynolds passed away. I had the privilege of being one of his graduate students, and much of what I know about what it mean...

Joshua and I thought our new typechecking algorithm for higher-rank polymorphism was easy to implement, but I have to admit that we weren...

Part of the reason for the silence on this blog is that it's been a very busy spring for me. I've got three new drafts to announce, ...