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

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

Hi,

Reminding that this week's LFCS seminar will start shortly:

  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.