Synechepedia

Homepages to watch

Andreas Rossberg

https://people.mpi-sws.org/~rossberg/index.html Developer of HaMLet and 1ML, working on WASM.

Bertie Spell

https://bertiespell.com/home

Philosophy, sociology, literary theory, blockchain, design.

Bob Atkey

https://bentnib.org/

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

https://www.engboris.fr/

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.

https://boarders.github.io/

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

https://gjoncas.github.io/

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

http://girard.perso.math.cnrs.fr/Accueil.html

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

https://team.inria.fr/partout/

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