\[
\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