\[
\newcommand{\ottnt}[1]{#1}
\newcommand{\ottsym}[1]{#1}
\newcommand{\ottmv}[1]{\mathit{#1}}
\newcommand{\func}[1]{\mathsf{#1}}
\newcommand{\Lin}[0]{\func{Lin}}
\newcommand{\Mny}[0]{\func{Mny}}
\newcommand{\Forget}[0]{\func{Forget}}
\newcommand{\Free}[0]{\func{Free}}
\newcommand{\Endo}[0]{\func{Endo}}
\newcommand{\mto}[1]{\xrightarrow{#1}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\catobj}[1]{\mathsf{Obj}(\cat{#1})}
\newcommand{\Obj}[1]{\catobj{#1}}
\newcommand{\catop}[1]{\cat{#1}^{\mathsf{op}}}
\newcommand{\sets}[0]{\mathsf{Set}}
\newcommand{\Set}[0]{\sets}
\newcommand{\mor}[1]{\mathsf{Mor}(\cat{#1})}
\newcommand{\Hom}[3]{\mathsf{Hom}_{#1}(#2,#3)}
\newcommand{\cur}[0]{\mathsf{cur}}
\newcommand{\curi}[0]{\mathsf{cur}^{-1}}
\newcommand{\app}[0]{\mathsf{app}}
\newcommand{\id}[0]{\mathsf{id}}
\newcommand{\injl}[0]{\mathsf{inj_l}}
\newcommand{\injr}[0]{\mathsf{inj_r}}
\newcommand{\pow}[1]{\mathcal{P}(#1)}
\newcommand{\oast}{⊛}
\]
The Symposium on the Logical Foundations of Computer Science is
underway. I am lucky enough to have given a talk. I presented my work
with Valeria de Paiva on full intuitionistic linear
logic and its categorical models. The paper can be found
here,
and my slides can be found
here.
The workshop is being held at the beautiful
Wyndham Hotel and Resort which
is quite literally on the beach. As you exit the hotel you see nothing
but a beautiful ocean view:
However, the con of this venue is that it’s expensive, and so I
decided to stay at the less amazing Hampton Inn, and commute over in
the morning. So far so good. For more information on the symposium
check out the webpage.
My talk went quite well, and I am happy that I was not as nervous
as I usually am; I think perhaps lecturing regularly has helped with
my nerves. After the talk I got a number of good questions which is
great. I always get nervous about not getting any.
One question was quite interesting which was “why hasn’t anyone
done the cut-elimination and categorical models for non-commutative
(full) intuitionistic logic?” I don’t know the answer to this
question, but perhaps it would be interesting to write it down.
I might post more later.
Leave a comment by sending me an Email