Seminario a Firenze

Yesterday, I gave a seminar in the Department of Philosophy in Florence.

If interested, here are the slides.

Workshop

For those interested, I want to signal the workshop Foundation of Mathematics for Computer-Aided Formalization. I’ve just registered for participation.

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 category theory. It also shows a semantics for the corresponding lambda-calculus.

The relation between the two semantics is exactly the Curry-Howard isomorphisms, which is not surprising.

The surprise is that the semantics is point-free, that is, no universe is needed to interpret terms. Or better, terms are not interpreted as elements but, rather, they generate a structure that keeps together the category where formulae and proofs are interpreted. This resembles somewhat Formal Topology (in more than one way, to say the truth).

In the immediate future, I want to relate this semantics with the one based on Heyting categories, and also with the Kripke-Joyal semantics which is based on Grothendieck topoi.

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 lambda-calculus whose types are the formulae and whose terms are the proofs.

In this period, I’m looking at the categorical models of intuitionistic logics and at the categorical models of typed lambda-calculi. It is folklore that these models are the same. In fact, this is false: they are strictly related, but essentially different. And there are a few surprises…

Soon, I will write a draft on these topics. Stay tuned if interested!

Today’s seminar

Today I spoke about Adpositional Grammars introducing them to my colleagues in Leeds.

This post is to whom is interested and wants to have a look at the slides.

AucTeX and XeLaTeX

When working with XeLaTex (the xelatex command) you need to compile the LaTeX source from a terminal (Unix/Linux/MacOS) or from the command prompt (Windows).

As I frequently use XeLaTeX and I edit LaTeX source with Emacs and AucTeX, I added a small customisation line in the .emacs file so that I can run the command inside Emacs, invoking Ctrl-C Ctrl-C and selecting XeLaTeX as the compiler. Here is the small command line to add to your .emacs file

(eval-after-load "tex"
  '(add-to-list 'TeX-command-list
     		'("XeLaTeX" "xelatex -interaction=nonstopmode %s"
		  TeX-run-command t t :help "Run xelatex") t))

Why do you want to use xelatex instead of latex or pdflatex?

Well, first because xelatex produces .pdf files as pdflatex but it allows for more registers: the stuff you don’t want to see, but which occasionally disturb you, especially when compiling complex documents like slides with Beamer plus a lot of fancy mathematical packages, e.g., XY-pic.

Second, xelatex together with fontspec allows to access and to use the native fonts of your system: in short, when publishers ask you to use the horrible Times New Roman instead of the “real” Times, well, you can just do it with a couple of declarations in the preamble!

Essentially, all TrueType fonts are supported, so you don’t have to perform strange TeX magic to use them in your documents (BTW, I’ve always had problems in doing those magic, at least on Windows machines).

Seminar announce

In the Proof Theory Seminars series, I will give a talk on Adgrams: categories and linguistics.

The seminar will take place in MALL 2, School of Mathematics, University of Leeds, at 3:00 pm, 26th October 2011.

In this talk, I will illustrate the formal model behind the work on structural linguistics I developed in cooperation with Dr. F. Gobbo. I will also introduce some ideas on how to apply those findings in the description of structural properties of mathematical theories.