{"id":84,"date":"2013-01-13T09:24:08","date_gmt":"2013-01-13T11:24:08","guid":{"rendered":"https:\/\/wp.ufpel.edu.br\/weit\/?page_id=84"},"modified":"2013-10-23T13:09:38","modified_gmt":"2013-10-23T15:09:38","slug":"minicursos","status":"publish","type":"page","link":"https:\/\/wp.ufpel.edu.br\/weit\/weit2013\/programacao\/minicursos\/","title":{"rendered":"Minicursos"},"content":{"rendered":"<h3><strong>Uma Introdu\u00e7\u00e3o ao C\u00e1lculo Lambda e Linguagens de Programa\u00e7\u00e3o Funcionais (Minicurso 1)<\/strong><\/h3>\n<h4><strong>Dr. RODRIGO MACHADO<\/strong><\/h4>\n<ul>\n<li><span style=\"text-decoration: underline\">Resumo<\/span>: C\u00e1lculo Lambda \u00e9 um formalismo originalmente proposto por Alonzo Church que visa descrever precisamente a defini\u00e7\u00e3o e aplica\u00e7\u00e3o de fun\u00e7\u00f5es. Assim como o modelo da M\u00e1quina de Turing, C\u00e1lculo Lambda \u00e9 um formalismo universal, permitindo a codifica\u00e7\u00e3o de qualquer algoritmo poss\u00edvel. Enquanto a M\u00e1quina de Turing serviu de inspira\u00e7\u00e3o para as linguagens de programa\u00e7\u00e3o imperativas, onde o estado do sistema \u00e9 composto por vari\u00e1veis e atualizado atrav\u00e9s comandos, C\u00e1lculo Lambda serviu de inspira\u00e7\u00e3o para as linguagens de programa\u00e7\u00e3o funcionais, onde programas s\u00e3o estruturados atrav\u00e9s de composi\u00e7\u00e3o de fun\u00e7\u00f5es. Este mini-curso tem por objetivo apresentar o modelo universal conhecido por C\u00e1lculo Lambda, assim como aspectos fundamentais de programa\u00e7\u00e3o em linguagens funcionais. Ser\u00e3o apresentados o C\u00e1lculo Lambda sem tipos, algumas propriedades da avalia\u00e7\u00e3o de termos lambda, a codifica\u00e7\u00e3o de diversos tipos de dados e uma breve apresenta\u00e7\u00e3o do C\u00e1lculo Lambda Tipado Simples, assim como sua conex\u00e3o com l\u00f3gica. Ser\u00e1 contextualizada a conex\u00e3o desses conceitos com caracter\u00edsticas de linguagens de programa\u00e7\u00e3o atuais.<\/li>\n<li><span style=\"text-decoration: underline\">Biografia<\/span>: Possui gradua\u00e7\u00e3o em Ci\u00eancia da Computa\u00e7\u00e3o pela Universidade Federal do Rio Grande do Sul (2002), mestrado em Computa\u00e7\u00e3o pela Universidade Federal do Rio Grande do Sul (2005) e doutorado em Computa\u00e7\u00e3o pela Universidade Federal do Rio Grande do Sul (2012). Tem experi\u00eancia na \u00e1rea de Ci\u00eancia da Computa\u00e7\u00e3o, com \u00eanfase em l\u00f3gicas e sem\u00e2ntica de programas, atuando principalmente nos seguintes temas: sem\u00e2ntica formal, modelos de computa\u00e7\u00e3o, sistemas de reescrita de grafos e linguagens de programa\u00e7\u00e3o funcionais.<\/li>\n<li><span style=\"text-decoration: underline\">Material<\/span>: fa\u00e7a o download dos slides da apresenta\u00e7\u00e3o\u00a0<a title=\"apresenta\u00e7\u00e3o\" href=\"https:\/\/wp.ufpel.edu.br\/weit\/files\/2013\/03\/RodrigoMachado-weit2013.pdf\" target=\"_blank\">aqui<\/a>. Para fazer o download da ferramenta usada para as demonstra\u00e7\u00f5es acesse este <a title=\"ferramenta\" href=\"http:\/\/www.inf.ufrgs.br\/~rma\/index.php?section=software&amp;lang=pt_BR\" target=\"_blank\">link<\/a>.<\/li>\n<\/ul>\n<hr \/>\n<h3><strong>Uma Introdu\u00e7\u00e3o \u00e0 Prova Interativa de Teoremas com Isabelle\/HOL (Minicurso 2)<\/strong><\/h3>\n<h4><strong>Dr. ALFIO RICARDO DE BRITO MARTINI<\/strong><\/h4>\n<ul>\n<li><span style=\"text-decoration: underline\">Resumo<\/span>: Tanto na Ci\u00eancia da Computa\u00e7\u00e3o como na L\u00f3gica Matem\u00e1tica, um assistente de prova ou um provador interativo de teoremas, \u00e9 um software que auxilia no desenvolvimento de provas formais atrav\u00e9s de uma colabora\u00e7\u00e3o homem-m\u00e1quina. Neste mini-curso, estaremos mostrando o sistema de especifica\u00e7\u00e3o e verifica\u00e7\u00e3o Isabelle\/HOL. Isabelle \u00e9 um sistema gen\u00e9rico para implementa\u00e7\u00e3o de formalismos l\u00f3gicos e Isabelle\/HOL \u00e9 a especializa\u00e7\u00e3o de Isabelle para (H)igher (O)rder (L)ogic, onde entendemos HOL atrav\u00e9s da seguinte equa\u00e7\u00e3o: HOL = Programa\u00e7\u00e3o Funcional + L\u00f3gica. Isabelle\/HOL inclui ferramentas poderosas para especifica\u00e7\u00e3o, como tipos de dados, defini\u00e7\u00f5es indutivas e fun\u00e7\u00f5es com pattern matching complexos. As provas s\u00e3o conduzidas com a linguagem estruturada de provas Isar (Intelligible semi-automated reasoning), que permite construir provas que sejam compreens\u00edveis tanto para pessoas como para m\u00e1quinas. Em especial, introduziremos as constru\u00e7\u00f5es necess\u00e1rias para especifica\u00e7\u00e3o e racioc\u00ednio sobre defini\u00e7\u00f5es de fun\u00e7\u00f5es recursivas e estruturas discretas como conjuntos, fun\u00e7\u00f5es e rela\u00e7\u00f5es. Como estudo de caso, mostraremos como aplicar estas ferramentas para a defini\u00e7\u00e3o e prova de teoremas envolvendo a sem\u00e2ntica formal de uma pequena linguagem de programa\u00e7\u00e3o. Exemplos incluir\u00e3o as abordagens tradicionais da sem\u00e2ntica denotacional, operacional e l\u00f3gica de Hoare.<\/li>\n<li><span style=\"text-decoration: underline\">Biografia<\/span>: Possui gradua\u00e7\u00e3o em Bacharelado em Matem\u00e1tica Aplicada \u00e0 Inform\u00e1tica pela Universidade Luterana do Brasil (1992), mestrado em Computa\u00e7\u00e3o pela Universidade Federal do Rio Grande do Sul (1994) e doutorado em Ci\u00eancia da Computa\u00e7\u00e3o pela Technische Universit\u00e4t Berlin (1999). Atualmente \u00e9 professor com dedica\u00e7\u00e3o exclusiva da Pontif\u00edcia Universidade Cat\u00f3lica do Rio Grande do Sul. Trabalha principalmente nos seguintes temas: m\u00e9todos formais, teoria das categorias, sistemas l\u00f3gicos na ci\u00eancia da computa\u00e7\u00e3o e prova interativa de teoremas.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Uma Introdu\u00e7\u00e3o ao C\u00e1lculo Lambda e Linguagens de Programa\u00e7\u00e3o Funcionais (Minicurso 1) Dr. RODRIGO MACHADO Resumo: C\u00e1lculo Lambda \u00e9 um formalismo originalmente proposto por Alonzo Church que visa descrever precisamente a defini\u00e7\u00e3o e aplica\u00e7\u00e3o de fun\u00e7\u00f5es. Assim como o modelo da M\u00e1quina de Turing, C\u00e1lculo Lambda \u00e9 um formalismo universal, permitindo a codifica\u00e7\u00e3o de qualquer [&hellip;]<\/p>\n","protected":false},"author":234,"featured_media":0,"parent":86,"menu_order":3,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-84","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/pages\/84","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/users\/234"}],"replies":[{"embeddable":true,"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/comments?post=84"}],"version-history":[{"count":12,"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/pages\/84\/revisions"}],"predecessor-version":[{"id":440,"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/pages\/84\/revisions\/440"}],"up":[{"embeddable":true,"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/pages\/86"}],"wp:attachment":[{"href":"https:\/\/wp.ufpel.edu.br\/weit\/wp-json\/wp\/v2\/media?parent=84"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}