Uma Introdução ao Cálculo Lambda e Linguagens de Programação Funcionais (Minicurso 1)

Dr. RODRIGO MACHADO

• Resumo: Cálculo Lambda é um formalismo originalmente proposto por Alonzo Church que visa descrever precisamente a definição e aplicação de funções. Assim como o modelo da Máquina de Turing, Cálculo Lambda é um formalismo universal, permitindo a codificação de qualquer algoritmo possível. Enquanto a Máquina de Turing serviu de inspiração para as linguagens de programação imperativas, onde o estado do sistema é composto por variáveis e atualizado através comandos, Cálculo Lambda serviu de inspiração para as linguagens de programação funcionais, onde programas são estruturados através de composição de funções. Este mini-curso tem por objetivo apresentar o modelo universal conhecido por Cálculo Lambda, assim como aspectos fundamentais de programação em linguagens funcionais. Serão apresentados o Cálculo Lambda sem tipos, algumas propriedades da avaliação de termos lambda, a codificação de diversos tipos de dados e uma breve apresentação do Cálculo Lambda Tipado Simples, assim como sua conexão com lógica. Será contextualizada a conexão desses conceitos com características de linguagens de programação atuais.
• Biografia: Possui graduação em Ciência da Computação pela Universidade Federal do Rio Grande do Sul (2002), mestrado em Computação pela Universidade Federal do Rio Grande do Sul (2005) e doutorado em Computação pela Universidade Federal do Rio Grande do Sul (2012). Tem experiência na área de Ciência da Computação, com ênfase em lógicas e semântica de programas, atuando principalmente nos seguintes temas: semântica formal, modelos de computação, sistemas de reescrita de grafos e linguagens de programação funcionais.
• Material: faça o download dos slides da apresentação aqui. Para fazer o download da ferramenta usada para as demonstrações acesse este link.

Uma Introdução à Prova Interativa de Teoremas com Isabelle/HOL (Minicurso 2)

Dr. ALFIO RICARDO DE BRITO MARTINI

• Resumo: Tanto na Ciência da Computação como na Lógica Matemática, um assistente de prova ou um provador interativo de teoremas, é um software que auxilia no desenvolvimento de provas formais através de uma colaboração homem-máquina. Neste mini-curso, estaremos mostrando o sistema de especificação e verificação Isabelle/HOL. Isabelle é um sistema genérico para implementação de formalismos lógicos e Isabelle/HOL é a especialização de Isabelle para (H)igher (O)rder (L)ogic, onde entendemos HOL através da seguinte equação: HOL = Programação Funcional + Lógica. Isabelle/HOL inclui ferramentas poderosas para especificação, como tipos de dados, definições indutivas e funções com pattern matching complexos. As provas são conduzidas com a linguagem estruturada de provas Isar (Intelligible semi-automated reasoning), que permite construir provas que sejam compreensíveis tanto para pessoas como para máquinas. Em especial, introduziremos as construções necessárias para especificação e raciocínio sobre definições de funções recursivas e estruturas discretas como conjuntos, funções e relações. Como estudo de caso, mostraremos como aplicar estas ferramentas para a definição e prova de teoremas envolvendo a semântica formal de uma pequena linguagem de programação. Exemplos incluirão as abordagens tradicionais da semântica denotacional, operacional e lógica de Hoare.
• Biografia: Possui graduação em Bacharelado em Matemática Aplicada à Informática pela Universidade Luterana do Brasil (1992), mestrado em Computação pela Universidade Federal do Rio Grande do Sul (1994) e doutorado em Ciência da Computação pela Technische Universität Berlin (1999). Atualmente é professor com dedicação exclusiva da Pontifícia Universidade Católica do Rio Grande do Sul. Trabalha principalmente nos seguintes temas: métodos formais, teoria das categorias, sistemas lógicos na ciência da computação e prova interativa de teoremas.