Seminário de Lógica Matemática

Towards Canonical Proofs for Second Order Intuitionistic Logic

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

Por Paolo Pistone (Université Claude Bernard Lyon 1).

In the last few years there has been a rise of interest towards the study of canonical proof systems. In standard proof systems, like natural deduction or sequent calculus, it is often the case that distinct formal derivations may represent, intuitively or semantically, the same proof. Instead, in a canonical system distinct derivations should ideally correspond to intuitively or semantically distinct proofs. Beyond its relevance for proof theory and the identity of proofs problem (when are two proofs the same?), the study of such systems is important also from the viewpoint of programming language theory: via the Curry-Howard correspondence, semantically equivalent proofs correspond to equivalent programs, that is, to programs computing the same function; canonical proof systems provide then methods to understand program equivalence, a crucial ingredient of program verification. Different techniques to obtain canonical proof systems exist in the literature, from focused proof-search to linear logic proof nets and combinatorial proofs. Our project aims at studying canonical proofs for System F, that is, for propositional intuitionistic second order logic, by combining focused proof search with recent results on the categorical semantics of polymorphism. As System F provides the abstract architecture for many functional programming languages, our long term goal is thus to devise new methods to understand program equivalence for such languages.


Transmissão via Zoom (pw: 919 4789 5133).

15h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional / CFCUL - Centro de Filosofia das Ciências da Universidade de Lisboa
Logótipo Mentimeter

Ação de formação para docentes e investigadores de CIÊNCIAS.

Neste curso ficarás a saber como te podes tornar um permacultor eficiente, produtivo e consciente! O curso está preparado para iniciantes na prática de permacultura.

Formação - Cultivar em Permacultura.

Químico a escrever fórmulas num quadro

Curso acreditado para efeitos de progressão na carreira dos professores do Ensino Básico e Secundário do Grupo 510 (CCPFC/ACC-118288/22), com candidaturas até 18 de maio.

Curso destinado a estudantes de Mestrado e de Doutoramento, bem como a profissionais que desenvolvam investigação científica na área da saúde.

Título/data/local do evento e fotografia do mar

Quais são os conceitos-chave para enfrentar os atuais desafios marinhos e costeiros? 

Representação de programação R

This course aims at providing students with basic knowledge of R programming, allowing them to manipulate and visualize data with R.

The conference focuses on "Algebra and its role in Computer Science", with special emphasis on the areas of study related to the work of M. V. Volkov, such as semigroups and automata.

Título/data/local do evento e fotografia do espaço

How far will you go? The IA Summer Program 2025 is your launchpad to the Universe - apply until 26 May!

Logótipo do Verão na ULisboa, sobre um fundo azul

Candidaturas a partir de 07 de abril!

Representação de programação R

This course aims at providing students with statistical knowledge and tools to manipulate, analyse and visualise biological data with R. Introduction to modeling, simulations and Bayesian statistics.

Workshop organizado pelo CEMS.UL - Centro de Estudos Matemáticos e pelo CAMGDS - Centro de Análise Matemática, Geometria e Sistemas Dinâmicos.

Título/data do evento e vários objetos museológicos

This course aims to provide an updated vision of the potential of museum collections for biodiversity research. More specifically, aims to present case studies on the value of museums and the use of collections and specimens in the 21st century, using new technologies and analytical methods.

Computability in Europe (CiE) is an interdisciplinary series of international conferences organised by the Association Computability in Europe (ACiE).

Título e datas do programa de estágios

Ready to explore research up close? Applications Deadline: 10 May.

Á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, com candidaturas até 02 de junho.

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

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

An international symposium that convenes researchers specializing in various disciplines focused on the terrestrial and marine flora and vegetation of the Macaronesian region (Azores, Madeira, Selvagens, Canary Islands, and Cabo Verde).

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

O curso visa dotar os formandos, com formação universitária nas mais diversas áreas do saber, 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.

Cientista a trabalhar com tubos de ensaio

Este curso forma profissionais para atividade na área das Análises Clínicas ou Patologia Clínica. 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.

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.

The conference aims to bring together key experts in the Medical Microwave Imaging (MMWI) field and will include invited talks, presentations and posters of peer-reviewed abstracts and conference papers, and workshops in satellite areas of research that are of interest to MMWI research.

Páginas