# Homepages to watch

## Andreas Rossberg

https://people.mpi-sws.org/~rossberg/index.html 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

http://www.lix.polytechnique.fr/Labo/Catuscia.Palamidessi/

Information theory, privacy, via logical lenses.

(Spouse of Dale Miller.)

## Callan McGill

PLT, computation, dependent types, category theory.

## Dale Miller

http://www.lix.polytechnique.fr/Labo/Dale.Miller/

Linear logic programming, proof theory, automated reasoning.

(Spouse of Catuscia Palamidessi.)

## Daniel Bünzel

http://erratique.ch/contact.en OCaml, Libre Software

## Drup’s Thingies

https://drup.github.io/ OCaml libraries and techniques

## Equivalent Exchange

https://equivalentexchange.blog/

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

http://www.cs.cmu.edu/~fp Linear logic, formal verification, type theory

## Giuseppe Longo

https://www.di.ens.fr/users/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

http://starsbeetlesandfools.blogspot.com/2012/06/suggested-readings-in-fantasy.html?m=1

## Jean-Yves Girard

Originator of

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

## Laura Crosilla

https://sites.google.com/view/lauracrosilla/home Type theory, constructivism, philosophy of mathematics

## Michael Cuffaro

http://www.michaelcuffaro.com/ Philosopher, computer scientists

## Neel Krishnaswami

## Paolo Pistone

http://logica.uniroma3.it/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).

## PARTOUT

Proof Automation and RepresenTation: a fOundation of compUtation and deducTion

## Roddy MacSween

Graduate student in CS who has built some useful ocaml web tools. https://roddymacsween.co.uk/

## 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*.

http://www.matfis.uniroma3.it/persone/docenti/docenti_beige.php?persona=71