| |
|
Description: |
The Curry-Howard-Lambek correspondence shows the deep connection between programs, proofs and morphisms in closed cartesian categories. It's natural to ask if similar results are true in other logics. Identifying the intuitionistic linear logic derivations up to the transformations in cut elimination, we obtain classes that spontaneously organize themselves into a monoidal category. Building on this we define a categorical semantics for intuitionistic linear logic and show that coherence spaces have the required categorical structure to model intuitionistic linear logic.
|
|
Date: |
|
| Start Time: |
11:30 |
|
Speaker: |
Carlos Fitas (UC|UP PhD student)
|
|
Institution: |
Universidade do Porto
|
|
Place: |
Sala 004, UP Math. Dept.
|
|
See more:
|
<Main>
<UC|UP MATH PhD Program>
|
|
