Homepages to watch

Andreas Rossberg Developer of HaMLet and 1ML, working on WASM.

Bertie Spell

Philosophy, sociology, literary theory, blockchain, design.

Bob Atkey

Researcher on PLT with a really fascinating mix of work.

My research is on programming languages. I use mathematical ideas and structure from logic, category theory, type theory, and denotational semantics to study programming languages and the systems they describe.

Boris Eng

Logic and computation, focused on Girard’s transcendental syntax

Catuscia Palamidessi

Information theory, privacy, via logical lenses.

(Spouse of Dale Miller.)

Callan McGill

PLT, computation, dependent types, category theory.

Dale Miller

Linear logic programming, proof theory, automated reasoning.

(Spouse of Catuscia Palamidessi.)

Daniel Bünzel OCaml, Libre Software

Drup’s Thingies OCaml libraries and techniques

Equivalent Exchange

a journey towards a personal philosophy. I don’t claim to have any great conclusions. I hope that with enough thrashing about, a gem of understanding may eventually be produced. I don’t wait to completely understand something before I write about it. If I am inspired to post a diagram or write a scrap of text, I do so. As a result, much of what I present here seems incomplete and muddled. It’s just a blog, after all.

Frank Pfenning Linear logic, formal verification, type theory

Giuseppe Longo Logic, computability, epistemology, evolutionary and organismal biology

Graham Joncas

on computational economics and formal philosophy

J.G. Keely

  • Fantastic and speculative fiction and comics, wonderful reviews and recommendations

Jean-Yves Girard

Originator of

  • System-F
  • Linear Logic
  • GoI & Proof Nets
  • Transcendental Syntax

Laura Crosilla Type theory, constructivism, philosophy of mathematics

Michael Cuffaro Philosopher, computer scientists

Neel Krishnaswami

Paolo Pistone

Researcher in Logic, studied under Girard.

My research interests are in the proof-theory of second order logic (System F) and linear logic (especially proof-nets).

Parametric polymorphism, the central topic of second order proof-theory, lies at the border between mathematics, computer science, and philosophy. It can be considered as the mathematical counterpart of the old philosophical problem of impredicativity. Also, polymorphism is a well-known tool of many programming languages and has deep connections with category theory (dinaturality, coherence theorems, fibrations).


Proof Automation and RepresenTation: a fOundation of compUtation and deducTion

Roddy MacSween

Graduate student in CS who has built some useful ocaml web tools.

Vito Michele Abrusci

Linear logic, proof theory, informatics. Has papers on topics unearthing the continuity of logic from ancient to post-modern: e.g., Girard cites is paper “Syllogisms and Linear Logic” in The Blind Spot.