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
Título do programa e representação de família numa carrinha

CIÊNCIAS associa-se, uma vez mais, a esta iniciativa, promovendo várias atividades.

Banner Meredith Ringel Morris HCI for AGI

15 de julho, 14h00: CIÊNCIAS recebe Meredith R. Morris, Diretora de Investigação em Interacção Humano-IA na Google DeepMind e Professora Afiliada na Universidade de Washington, para uma palestra imperdível sobre um dos temas mais debatidos e transformadores da atualidade: o caminho rumo à Inteligência Artificial Geral (AGI).

Título e datas do programa de estágios

Preparados para explorar a investigação de perto?

Águas subterrâneas

Curso acreditado para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 420 e 520.

Um workshop com o objetivo de reunir académicos que abordam a história da ecologia - e a evolução da própria disciplina - a partir de uma variedade de perspetivas.

Cardume

Seminário no âmbito do Doutoramento em Ciências do Mar, por Inês Pereira.

Pormenor de mecanismo de relógio

Concerto no âmbito do programa Música na Universidade de Lisboa.

Orquestra

Concerto no âmbito do programa Música na Universidade de Lisboa.

Banner Ser Cientista

A 10.ª edição do Ser Cientista realiza-se entre 21 e 25 de julho - vem investigar connosco!

Título e data da iniciativa

A iniciativa conta com a participação do MARE - Centro de Ciências do Mar e do Ambiente e do LASIGE Computer Science and Engineering Research Centre.

Aluna a utilizar um computador portátil

A Escola Doutoral Unite! Widening visa apoiar diretamente estudantes de doutoramento que realizem investigação numa das quatro áreas estratégicas selecionadas pelo projeto - as candidaturas decorrem até 26 de julho.

Pormenor de lâmpada

Candidaturas a decorrer de 01 a 30 de setembro.

Microplásticos no ocerano

O curso procura 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, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

Logótipo do evento, sobre fotografia dos Açores

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Quatro investigadores num laboratório

O curso visa capacitar investigadores, docentes e técnicos para integrar os princípios da economia circular em ambientes laboratoriais académicos - candidaturas até 16 de setembro.

Três investigadores num laboratório

O curso visa capacitar profissionais para aplicar os princípios da economia circular em ambientes laboratoriais industriais, promovendo práticas sustentáveis e eficientes - candidaturas até 17 de setembro.

Composição de imagens relativas à área das ciências forenses

O curso visa dotar os formandos com os conhecimento necessários à integração de equipas profissionais multidisciplinares nas áreas Médico-Legais e Forenses, em Laboratórios ou Serviços Médico-Legais e Forenses - candidaturas até 27 de julho.

Logótipo do evento

Um evento promovido pelo Departamento de Física da Faculdade de Ciências da ULisboa, com um duplo objetivo: valorizar a diversidade e excelência da formação dos doutorados e promover um espaço de diálogo direto entre empresas e estudantes.

Cientista a trabalhar com tubos de ensaio

Os participantes neste curso irão adquirir os conhecimentos essenciais à integração de equipas profissionais multidisciplinares na área das Análises Clínicas/Patologia Clínica, em laboratórios privados, públicos, hospitalares ou do Estado - candidaturas até 27 de julho.

Saída de campo (Geologia)

O curso, com candidaturas até 20 de julho, convida os professores do Ensino Básico e Secundário a explorar a Geologia a partir das rochas que afloram nas imediações da sua escola.

Gotas de água

O curso visa capacitar os formandos para a aplicação dos índices de qualidade ecológica utilizados na avaliação da qualidade ambiental em sistemas de transição, no âmbito da Diretiva Quadro da Água (DQA) - candidaturas até 31 de agosto.

Astronauta, banhado pela luz solar, no meio de uma floresta

Candidaturas até 30 de julho - um evento único, que reunirá estudantes de mestrado e doutoramento com investigadores e líderes da indústria de toda a Europa para uma experiência inesquecível.

Lupa e caneta sobre página com texto e gráfico

O curso visa dar formação inicial a estudantes de pós-graduação sobre o processo de escrita, submissão e publicação de trabalhos científicos, focando principalmente a publicação de artigos científicos em revistas internacionais com revisão por pares.

Iconografia relacionada com a temática do curso

O curso fornece uma exploração aprofundada de isótopos estáveis como uma ferramenta valiosa em Ecologia, usando assinaturas isotópicas para rastrear processos ecológicos e revelando insights sobre o ciclo de nutrientes e água, interações de espécies e condições ambientais em diversos ecossistemas e comunidades.

Composição de três imagens relativas à área da deteção remota

2.ª edição do curso, com candidaturas até 18 de outubro.

Páginas