RSS Meetup

Agda as a Proof Assistant

Transmissão através de Videoconferência

Speaker: Bernardo Almeida (LASIGE, DI/FCUL).

Where: https://tertulia.di.fc.ul.pt/RSSmeetup.

Abstract: In this talk, we will overview Agda and see how to use it as a proof assistant. Agda is a dependently typed programming language whose powerful type system allows to specify and prove properties. Agda exploits the relation between programs and proofs, the so-called Curry-Howard correspondence, which means that we can interpret propositions as types, and proofs as programs. We will go through the book "Programming languages foundations in Agda" by Philip Wadler, Wen Kokke, and Jeremy Siek (plfa.github.io), introduce Agda and see some examples.

Bio: Bernardo Almeida is a PhD student at the Faculty of Sciences, University of Lisbon, and a student researcher at LASIGE. He received his BSc and MSc both in Computer Science, from the University of Lisbon. Currently, his main research interests are type systems and programming languages.

Agda as a Proof Assistant

15h00
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

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 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

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.

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.

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.

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

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

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