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
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
Curry-Howard
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
Olivia’s Website
Olivia Caramello has now a website where she explains her research activity and, in particular, the unification project.
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