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
Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados - candidaturas até 12 dezembro.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos - candidaturas até 19 de dezembro.

Imagem exemplificativa da área da deteção remota

Este curso avançado tem como objetivo fornecer acesso e ferramentas para a aquisição e processamento de dados de deteção remota para diferentes aplicações, usando imagens multiespectrais de satélite, drone, terrestres e LiDAR, com foco na caracterização da vegetação e da paisagem, bem como das suas mudanças ao longo do tempo - candidaturas até 19 de dezembro.

Imagem abstrata

Neste curso, será promovida uma abordagem multidisciplinar, apresentando as descobertas mais recentes sobre o tema e desafiando a forma tradicional de considerar as associações simbióticas como exceções e não como a regra - candidaturas até 09 de janeiro.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.

Páginas