Mathematical Logic Seminar

Dissymetrical Linear Logics

Sala 6.2.33, Ciências ULisboa (com transmissão via Zoom)

Por Jean-Baptiste Joinet (Université Jean Moulin, Lyon 3, France).

A good way to introduce Linear Logic is to present it through the so called Curry-Howard correspondence (proofs-as-programs / cut elimination-as-computation / formulas-as-types). Indeed, in that frame, Linear Logic can be seen as a magnifying glass thanks to which the computational process (cut-elimination of intuitionistic or classical proofs) appears decomposed into specific, more elementary dynamical effects (which, in the dynamic of intuitionistic or classical proofs, are undistinguishable and remain mixed up).

The diversity of Linear Logic connectives (multiplicative, additive and exponential ones, and their variants as functorial exponentials, specialized exponentials etc) mirrors, at the level of types alias formulas (i.e. connectives and the rules involving them), that decomposition of the dynamic of proofs.

From that perpective, the various ways one is able to interpret (though translations) ``intuitionistic'' and ``classical'' Logic (respectively) in Linear Logic, have to be thought as catching statically some features of the respective possible dynamics of both logics.

Typically, when one interprets ``intuitionistic'' and ``classical'' implications in Linear Logic, the difference between them is not caught at the level of the implication connective itself (i.e. by distinguishing a classical and an intuitionistic implications as one sometimes does in the frame of the “Logical Ecumenism’’), but by using differently the modalities of Linear Logic: ``!'' and ``?’’. Statically, those modalities (called the exponentials) serve to indicate the (potential) use of left and right structural rules, respectively. Dynamically, structural rules are the source of the non linear, “structural” part of the computation (notably: duplication of code, erasing of code etc). Whence the slogan : “The exponentials are thus in charge of the structural part of the computation”.

In my talk, I will only (or mainly) focus on the exponentials “!” and “?” of Linear Logic. After presenting the four structural effects they are in charge of (in the simpler case of Intuitonistic Linear Logic, ILL), I will analyse the way “!” and “?” interact (statically and dynamically) and try to measure how far they are – or not – independent.

That investigation results in creating ``intermediate exponentials'' that I use to design computational systems of linear logic which are ``intermediate'' between Intuitionistic LL (ILL) and Classical LL (CLL). Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in CLL, in order to get ``!'' and the resulting ``?'' playing well differentiated roles -- and this without to loose the computational properties (closure by cut-elimination, atomizability of identity axioms). Four main systems are designed (Dissymetrical LL, semi-functorial Dissymetrical LL, semi-specialized Dissymetrical LL, bi-conclusion LL).

If times allows, I will then show how to us Dissymetrical LL (DLL) as a tool to design multi-conclusion Intuitionistic sequent calculi.


Transmissão via Zoom.

15h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

RSS Meetup, por Nuno Lopes (IST, ULisboa).

Seminário do Departamento de Física de Ciências ULisboa, por Henrique Leitão (DHFC-FCUL, PI RUTTER ERC AdG).

Logótipo do evento

No dia 04 de abril, pelas 14h30, será gravado um episódio em direto do podcast "A Escala do Clima" de Filipe Duarte Santos (Professor Jubilado de CIÊNCIAS).

Fotografia de aluna

Uma iniciativa aberta a toda a comunidade académica da ULisboa.

Fotografia de coleção de insetos

The course includes several case studies of insect adaptation, and the most recent overview on insect evodevo, plasticity, ecophysiological responses and conservation under global change.

Título/data/local do evento e fotografia aérea de vias urbanas

Conferência da redeMOV, por Gabriel Costa Valença.

Logótipo CIE

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.

Logótipos do evento/Ciências ULisboa/AEFCL e data do evento, sobre fotografia de edição anterior

O maior evento de empregabilidade de CIÊNCIAS, a decorrer nos dias 08 e 09 de abril.

Seminário do Centro de Física Teórica e Computacional, por João Neves (CFTC).

RSS Meetup, por Rodrigo Bruno (IST, ULisboa).

Título do evento

A collaborative initiative supported by five Portuguese research centers, aimed at strengthening and connecting the geometry research community in Portugal.

Equipa da Raiz Vertical Farms

Uma Experiência Única sobre Agricultura Urbana e Energia Renovável.

Título/data/local do evento e fotografia da cidade de Lisboa

The conference aims to bring together students and young researchers working in Mathematics, Statistics, and Applications with a view to fostering discussions and collaborations amongst participants.

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Amidou Sorgho (Instituto de Astrofísica de Andalucía - IAA-CSIC, Spain).

Título "Para um ensino humanista das ciências" e logótipos das entidades organizadoras

O evento tem como tema principal "Para um ensino humanista das ciências" e conta com a participação de vários professores de CIÊNCIAS.

Microplásticos em suspensão no oceano

O curso tem como objetivo dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos - candidaturas até 22 de março.

Banner do Dia de Ciências 2025

A 29 de abril assinalamos o 114.º aniversário de CIÊNCIAS.

Junte-se a nós no Grande Auditório de CIÊNCIAS para uma tarde de celebração que reúne toda a comunidade da Faculdade.

Fotografia de fábrica a emitir poluição para a atmosfera

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems.

Logótipo C-Academy

O curso oferece uma base sólida sobre os fundamentos e práticas essenciais para proteger sistemas e dados num mundo cada vez mais digital - candidaturas até 13 de abril.

Banner Dia Aberto de CIÊNCIAS 2025.

Bem-vindos a Ciências ULisboa!

Um concurso de programação dirigido aos alunos do ensino secundário (11.º e 12.º anos), que visa promover a prática e o gosto pela programação.

Fotografia de Chapim-azul

The goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

Mão a segurar em globo de vidro

Curso acreditado pelo CCPFC para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 230, 420, 510, 520 e 560, com candidaturas até 30 de abril.

Título/data/local do evento, logótipos das entidades organizadoras e fotografia de peixe

The event aims to facilitate the exchange of information and knowledge among professionals to advance the understanding, collaboration and capabilities of aquaculture to respond to the impact of climate change in a rapidly changing global environment.

Uma oportunidade única para interagir com a comunidade global de computação científica, com inscrições (preço reduzido) até 02 de maio.

Páginas