Mathematical Logic Webinar

Short introduction by example to Coq

Transmissão através de Videoconferência

Speaker: Jaime Gaspar (Centro de Matemática e Aplicações - CMA, FCT, UNL).

Abstract: Proof assistants are computer programs that help mathematicians to prove theorems and to formally verify the correctness of proofs. Proof assistants are nowadays one of the more exciting areas in the intersection of mathematical logic and computer science. For example, one particularly exciting achievement is the formal verification of the proof of the four colour theorem using the proof assistant Coq. In this talk we give a very elementary introduction to Coq by means of a very simple example: the proofs of the theorems (1) if ≤ is a non-strict partial order, then < defined by x < y ↔ x ≤ y ∧ x ≠ y is a strict partial order; (2) if < is a strict partial order, then ≤ defined by x ≤ y ↔ x < y ∨ x = y is a non-strict partial order. Then we end by discussing what is achieved with this kind of formal verification. We keep this talk very short, simple and sweet.


Zoom Meeting | Meeting ID: 890 8479 3299 | Password: 409604

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Logótipo do Dia Internacional da Matemática

Atividades a decorrer em CIÊNCIAS nos dias 14 e 19 de março.

Título "Jornadas de Matemática" e logótipos das entidades envolvidas

O Departamento de Matemática e o Núcleo de Estudantes de Matemática e Matemática Aplicada associam-se às celebrações do Dia Internacional da Matemática.

Planta

As candidaturas terminam a 20 de março, estando previstos vários eventos de matchmaking para ajudar os participantes a encontrar parceiros para os seus projetos.

Título "Cybersecurity Executive Program Edição 2025", sobre um fundo em tons de verde

Candidaturas a decorrer - desconto early bird em duas fases (até 15 de fevereiro e até 28 de fevereiro).

Reitoria da ULisboa

O ato eleitoral decorrerá nos dias 31 de março e 01 de abril de 2025.

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

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

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.

Banner do Dia de Ciências 2025

A 29 de abril de 2025 (terça-feira) assinalamos o 114.º aniversário da Ciências ULisboa.

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.

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.

Banner Dia Aberto de CIÊNCIAS 2025.

Bem-vindos a Ciências ULisboa!

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

Páginas