Marco Benini

Point-free semantics

Following the Marie Curie Fellowship in Leeds which ended in March, I have finished to write the long and complex report about my findings in that sabbatical period. The report … Continue reading

July 2, 2013 · Leave a comment

Curry-Howard II

A few days ago, I gave a talk in the Logic Seminar at Leeds. The slides are available at┬áleeds14102012. Essentially, it shows a semantics for full first-order intuitionistic logic in … Continue reading

November 22, 2012 · Leave a comment


The Curry-Howard isomorphism relates lambda-calculus with intuitionistic logic. Essentially, it says that to every variant of intuitionistic logic (propositional vs predicative, first-order, second-order, weak higher-order, full higher-order) corresponds a typed … Continue reading

December 27, 2011 · Leave a comment

Olivia’s Website

Olivia Caramello has now a website where she explains her research activity and, in particular, the unification project.

September 6, 2011 · 1 Comment

Order (and small disorder)

In most textbooks, one finds that a category represents a preorder exactly when there is at most one arrow between any pair of objects. But, surprisingly, the same is told … Continue reading

March 29, 2011 · Leave a comment