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
Logótipos de Ciências ULisboa/GAPsi e calendarização das palestras

A palestra visa apoiar o estabelecimento de planos de carreira (académicos e profissionais) e de vida.

Lisbon Webinar in Analysis and Differential Equations, por Damião Araújo (Universidade Federal da Paraíba).

Título/data/local do evento, logótipos das entidades participantes e fotografia de céu nublado

A 3.ª edição do workshop, dedicada à modelação e validação de processos de alta resolução, pretende abordar a modelação de fogos florestais e de eventos extremos de temperatura, precipitação e vento, tais como ondas de calor, secas, inundações, ciclones pós-tropicais e agitação marítima.  

Imagem abstrata

Um evento pioneiro que marca o lançamento do Programa para a Promoção da Saúde Mental no Ensino Superior na ULisboa. Ao longo do evento, será apresentada uma plataforma inovadora que reunirá recursos e iniciativas destinadas a prevenir e abordar questões relacionadas com a saúde mental e o bem-estar.

Título/data/local do evento, logótipos da entidade organizadora e fotografia de mãos na água

Encontro Alumni ULisboa 2024 - a inscrição é obrigatória, tendo um preço simbólico para apoiar o projeto Bolsas Alumni Solidário.

Data Science Seminar, por Helena Aidos (LASIGE/DI-FCUL).

Aula aberta no âmbito da Unidade Curricular "Da Revolução Científica à Big Science: Viagens e Expedições Científicas".

Título/data/local do evento e pintura representativa do Professor Bento Murteira

A sessão de homenagem inclui o lançamento de uma nova edição do livro Estatística: Inferência e Decisão, anteriormente editado pela Imprensa Nacional-Casa da Moeda, e atualmente esgotado.

Seminário do Centro de Física Teórica e Computacional, por Jorge Vieira (Departamento de Física, Instituto Superior Técnico, Universidade de Lisboa, Portugal).

Título/data/local do evento e logótipos das entidades organizadoras

Investigadores das áreas de antropologia dentária e antropologia debatem questões sobre a investigação em restos ósseos encontrados em escavações arqueológicas com impacto na história.

Título/data da iniciativa e logótipo Ciência Viva

CIÊNCIAS participa, uma vez mais, na Semana da Ciência e da Tecnologia, promovendo diversas atividades.

Faz uma equipa, completa os nossos desafios e mostra que és um verdadeiro mestre da sustentabilidade!

Todos nós utilizamos energia na nossa vida. Mas será que consegues reconhecer de onde é que ela vem? E os diferentes tipos de energia?

Seminário de Lógica Matemática, por Alberto Naibo (Université Paris 1 Panthéon-Sorbonne, IHPST).

Já te questionaste como é que uma turbina eólica funciona? E que tal criar uma tua?

Geometry and Physics Seminar, por Nicola Bellumat (CMAFcIO).

Seminário em Biologia Humana e Ambiente, por Deodália Dias (Departamento de  Biologia  Animal - FCUL / CESAM_Ciências).

Será que conheces todas as utilidades do Sol?

Ciência fresquinha? Temos. Uma bebida a acompanhar? Também!

Conferência do Centro Interuniversitário de História das Ciências e da Tecnologia, por Gemma Cirac-Claveras (Institut d'Història de la Ciència - Barcelona).

Logótipos de Ciências ULisboa/GAPsi e calendarização das palestras

Uma conversa sobre regulação emocional.

Nesta atividade será possível visitar alguns laboratórios do MARE, de modo a perceber o seu funcionamento e a investigação que aí é conduzida.

Será que sabes fazer a reciclagem? Será que conheces todos os 10 Rs da sustentabilidade?

A inteligência artificial (IA) tem estado no centro das atenções devido ao seu rápido desenvolvimento e potencial transformador em todas as áreas da sociedade, nomeadamente no sector da educação.

Uma viagem em que os visitantes terão a oportunidade de conhecer o LIP e os lugares para onde viajamos diariamente no nosso trabalho - os lugares onde estão instaladas as nossas experiências, de onde chegam os dados que analisamos, onde estão (ou estarão) instalados os detetores que construímos, onde é aplicada a investigação que se faz no LIP.

Páginas