The Curious Engineer

All blogs / Functional / PL theory

Semantic Domain

semantic-domain.blogspot.com

Functional / PL theoryCompilers

’10’15’20’25
Posts
107 from 5 Nov 2010 to 8 Jun 2026
Posting
now and then (2 in the last year)
Kind
personal blog
Feed
https://semantic-domain.blogspot.com/feeds/posts/default

2026 2

  1. QTCat: Queer and Trans People in Category Theory
  2. Bidirectional Typechecking That Does Not Stop

2025 1

  1. Finally...

2024 1

  1. How to Read Papers

2023 3

  1. The Ackermann-Péter Function in Gödel's T
  2. Actually, We Will Read Your Thesis
  3. Linear-time parser combinators

2022 6

  1. CN: Verifying Systems C Code with Separation-Logic Refinement Types
  2. Two Papers about Refinement Types
  3. The Golden Age of PL Research
  4. Fold Considered Annoying
  5. Simple Type Inference for System F
  6. Static typing vs. Dynamic Typing vs. Dana Scott

2021 6

  1. What is a programming language?
  2. Obliteratingly Fast Parser Combinators
  3. POPL till you DROPL
  4. Design Benchmarks
  5. Postdoctoral opening in the TypeFoundry project
  6. Five (and a Half) Derivatives in Language Theory

2020 4

  1. TypeFoundry: new ERC Consolidator Grant
  2. Church Encodings, Inductive Types, and Relational Parametricity
  3. PLDI 2020 Conference Report
  4. Thought Experiment: An Introductory Compilers Class

2019 8

  1. Every Finite Automaton has a Corresponding Regular Expression
  2. New Draft Paper: Survey on Bidirectional Typechecking
  3. On the Relationship Between Static Analysis and Type Theory
  4. Michael Arntzenius on the Future of Coding Podcast
  5. All Comonads, All The Time
  6. Implementing Inverse Bidirectional Typechecking
  7. Inverting Bidirectional Typechecking
  8. Some Paper Announcements

2018 5

  1. Polarity and bidirectional typechecking
  2. Category Theory in PL research
  3. The Worm Ouroboros
  4. A Typed, Algebraic Approach to Parsing
  5. Are functional programs easier to verify than imperative programs?

2016 7

  1. HOPE 2016 Talk Summaries
  2. Löb's theorem is (almost) the Y combinator
  3. Life Update: Moving to Cambridge
  4. The Essence of Event-Driven Programming
  5. Postdoctoral Position in Recursion, Guarded Recursion and Computational Effects
  6. Agda is not a purely functional language
  7. Datafun: A Functional Datalog

2015 7

  1. Error Handling in Menhir
  2. FRP without Space Leaks
  3. How to implement a spreadsheet
  4. Abstract Binding Trees, an addendum
  5. Abstract Binding Trees
  6. New Draft: Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types
  7. Midlands Graduate School 2015

2014 13

  1. Garbage collection and purity
  2. Quote of the Day
  3. Curry-Howard for GUIs: Or, User Interfaces via Linear Temporal, Classical Linear Logic
  4. Integrating Linear and Dependent Types at POPL 2015
  5. Focusing is not Call-by-Push-Value
  6. Two Drafts on Dependent Types
  7. PhD opportunities at the University of Birmingham
  8. Gödel's Ontological Argument
  9. From DPLL(T) to Sequent Calculus
  10. Papers I'm reading
  11. 2014 Midlands Graduate School
  12. Retiring a joke
  13. OBT 2014

2013 10

  1. PhD Opportunities at the University of Birmingham
  2. Antimirov Derivatives for Regular Expressions
  3. What Declarative Languages Are
  4. Internalizing Parametricity at CSL 2013
  5. Papers at ICFP 2013
  6. Strong Normalization without Logical Relations
  7. John C. Reynolds, June 1, 1935 - April 28, 2013
  8. Thanks to Olle Fredriksson
  9. Spring Things
  10. Interview with John Reynolds

2012 15

  1. Total Functional Programming in a Partial Impure Language
  2. The Geometry of Interaction, as an OCaml program
  3. Polymorphism and limit-colimit coincidence in reactive languages
  4. When it rains, it pours
  5. New Draft: Simple and Efficient Higher-Order Reactive Programming
  6. An astonishing isomorphism
  7. A Computational Lambda Calculus for Applicative Functors
  8. An ML implementation of match compilation
  9. Pattern compilation made easy
  10. Category Theory for Computing Science now free for download!
  11. A Relationally Parametric Model of the Calculus of Constructions
  12. Superficially Substructural Types at ICFP 2012!
  13. Djikstra's Shunting Yard Algorithm
  14. Superficially Substructural Logic
  15. Michael Dummett

2011 18

  1. Adding Equations to System F, at ESOP 2012
  2. Updata
  3. Adding Equations to System F
  4. Higher-Order Functional Reactive Programming in Bounded Space
  5. Radical predicativism
  6. The most surprising paper at ICFP
  7. Functional Programming, Program Transformations, and Compiler Construction
  8. A new lambda calculus for bunched implications
  9. Functional Programming as a Particular Use of Modules
  10. Termination of guarded recursion
  11. Semantics of a weak delay modality
  12. Guarded recursion with a weaker-than-Nakano guard modality
  13. The constructive lift monad
  14. ICFP 2011
  15. GUI Programming and MVC
  16. Models of Linear Logic: Length Spaces
  17. A Semantic Model for GUI Programs
  18. Ultrametric Semantics of Reactive Programs

2010 1

  1. Research notes