Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have an LFCS seminar tomorrow:

  Tuesday, 07 Jul, 4.10pm
  Pablo Donato, Charles University, Prague

  The seminar will take place in-person only.

We're synchronising the seminar time with the teaching timetable, and
plan to start the talk at the advertised time, so please arrive a minute or 
two
earlier.


In detail:

----------------------------------------------------------------------
Pablo Donato, Charles University, Prague
https://pablogician.refl.fr/

  Tue, 07 Jul, 4.10pm
  Venue: IF G.03


Title: Towards a Curry-Howard correspondence for existential graphs

Abstract

In this talk, I will introduce "scroll nets", a novel diagrammatic
formalism for representing proofs and programs. As the name
indicates, it is based on the "scroll", a topological notation for
logical implication invented by Charles S. Peirce at the end of the 19th
century for his system of existential graphs (EGs). In order to obtain a
proper notion of static proof object from the inference rules of EGs, we
add on top of the scroll a graphical syntax inspired by proof nets which
turns out to be an instance of Milner's notion of bigraph, thus also
enjoying an algebraic term syntax.


I will first motivate the diagrammatic notation from a philosophical
standpoint, arguing that it captures the smallest motions of
deductive reasoning in a very natural way, abstaining from any
symbolic means of representation. I will then show how to express
proofs in minimal implicative logic by simulating the rules of natural
deduction. Through the Curry-Howard correspondence, this will lead
us to identify a notion of detour that seems to generalize that of
simply-typed lambda-calculus. I will present ongoing work to provide
operational and denotational semantics to scroll nets, as well as an
adaptation of the normalization-by-evaluation technique to this new
setting. If time remains, I will sketch how to capture: 1. classical
logic and intuitionistic disjunction by considering a horizontal
generalization of the scroll first proposed by Oostra; 2.
intuitionistic subtraction through a further vertical
generalization of my own.

----------------------------------------------------------------------

Upcoming seminars:
------------------
07 Aug, Friday 2pm: Anindya De, University of Pennsylvania


If you would like to propose a speaker, or speak yourself, please contact me.
The seminar webpages:
http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,
Ohad.
The University of Edinburgh is a charitable body, registered in Scotland, 
with registration number SC005336. Is e buidheann carthannais a th’ ann an 
Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.