% (find-LATEX "2023-1-LA-plano-de-curso.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2023-1-LA-plano-de-curso.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2023-1-LA-plano-de-curso.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2023-1-LA-plano-de-curso.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2023-1-LA-plano-de-curso.pdf"))
% (defun e () (interactive) (find-LATEX "2023-1-LA-plano-de-curso.tex"))
% (defun o () (interactive) (find-LATEX "2023-1-C2-plano-de-curso.tex"))
% (defun u () (interactive) (find-latex-upload-links "2023-1-LA-plano-de-curso"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2023-1-LA-plano-de-curso.pdf"))
%          (code-eec-LATEX "2023-1-LA-plano-de-curso")
% (find-pdf-page   "~/LATEX/2023-1-LA-plano-de-curso.pdf")
% (find-sh0 "cp -v  ~/LATEX/2023-1-LA-plano-de-curso.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2023-1-LA-plano-de-curso.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2023-1-LA-plano-de-curso.pdf
%               file:///tmp/2023-1-LA-plano-de-curso.pdf
%           file:///tmp/pen/2023-1-LA-plano-de-curso.pdf
%  http://anggtwu.net/LATEX/2023-1-LA-plano-de-curso.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2023-1-LA-plano-de-curso" "laplc")

% «.defs»	(to "defs")
% «.title»	(to "title")
% «.links»	(to "links")




\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\usepackage{tikz}
\usepackage{longtable}                 % (find-es "tex" "longtable")
%
\usepackage{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
% (find-es "tex" "geometry")
\begin{document}


% «defs»  (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")

\def\u#1{\par{\footnotesize \url{#1}}}

\def\drafturl{http://anggtwu.net/LATEX/2023-1-LA.pdf}
\def\drafturl{http://anggtwu.net/2023.1-LA.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}



\begin{center}
UFF/CAMPUS DE RIO DAS OSTRAS

Instituto de Humanidades e Saude

Departamento de Ciências da Natureza

Eduardo Nahum Ochs - SIAPE 1669224

\bsk

{\bf Plano de curso da disciplina ``$λ$-Cálculo, Lógicas

e Linguagens de Programação'' (RCN00049)}

2023.1

\end{center}




\section{Objetivo, ementa e conteúdo programático}

O objetivo do curso, a ementa e o conteúdo programático do curso estão
abaixo. A ementa e o conteúdo programático também podem ser
consultados neste link:

%    https://app.uff.br/graduacao/quadrodehorarios/
\url{https://app.uff.br/graduacao/quadrodehorarios/}

\subsection{Objetivo do curso}

% (find-es "puro" "ementa-e-programa-LA")

Exercitar traduções entre várias linguagens, algumas mais abstratas
(semânticas formais, teoremas) e outras mais concretas (casos
particulares, diagramas finitos).

\subsection{Ementa}

\noindent

\noindent
Matemática Discreta com objetos finitos. \\
$λ$-cálculo. \\
Categorias. \\
Set e ordens parciais como categorias. \\
Lógica intuicionista pra crianças. \\
Curry-Howard. \\
Semânticas categóricas para crianças. \\
Algumas linguagens funcionais (Plzoo). \\

\subsection{Conteúdo programático}

\noindent
1. $λ$-cálculo e Lógica Proposicional. \\
1.1. Matemática Discreta com objetos finitos. \\
1.2. Set comprehension e quantificadores. \\
1.3. Notação $λ$, tipos e $λ$-cálculo tipado. \\
1.4. Redução e confluência. \\
1.5. Lógica Proposicional Intuicionista (IPL). \\
1.6. Introdução ao Isomorfismo de Curry-Howard. \\
2. Modelos para Lógica Proposicional Intuicionista. \\
2.1. Álgebras de Heyting. \\
2.2. Tautologias, teoremas, sistemas dedutivos. \\
2.3. Contra-modelos. \\
2.4. Tableaux. \\
2.5. Topologias. \\
2.6. Modelos de Kripke. \\
2.7. Lógicas modais. \\
2.8. Interpretação de IPL na lógica modal S4. \\
2.9. Interpretação de S4 em topologias. \\
3. Categorias. \\
3.1. Categorias. \\
3.2. Set e ordens parciais como categorias. \\
3.3. Terminais, iniciais, produtos e coprodutos. \\
3.4. Dualidade. \\
3.5. Unicidade módulo isomorfismo. \\
3.6. Funtores. \\
3.7. Transformações naturais. \\
3.8. Adjunções e exponenciais. \\
3.9. Categorias Cartesianas Fechadas. \\
3.10. $λ$-cálculo em Categorias Cartesianas Fechadas. \\
3.11. Semânticas Categóricas. \\
3.12. Isomorfismo de Curry-Howard. \\
4. Linguagens Funcionais. \\
4.1. Lisp. \\
4.2. Introdução ao Lua. \\
4.3. Implementação de um mini-Lisp. \\
4.4. Eager evaluation e lazy evaluation. \\
4.5. Implementação de thunks e lazy evaluation. \\


\section*{Plano de curso (cronograma)}

% «plano-de-curso»  (to ".plano-de-curso")
% (c2m231plcp 2 "plano-de-curso")
% (c2m231plca   "plano-de-curso")

\begin{longtable}{llp{9cm}}
 1 & 03/abr & Set comprehensions. Redução e confluência. Notação $λ$. \\
 2 & 10/abr & \it Feriado. \\
 3 & 17/abr & Matemática Discreta com objetos finitos. Álgebras de Heyting. Tautologias. \\
 4 & 24/abr & Tipos e $λ$-cálculo tipado. \\
 5 & 01/mai & \it Feriado. \\
 6 & 08/mai & Lógica Proposicional Intuicionista (IPL). Introdução ao Isomorfismo de Curry-Howard. \\
 7 & 15/mai & Teoremas e sistemas dedutivos. Contra-modelos. Tableaux. \\
 8 & 22/mai & Topologias. Lógicas modais. Modelos de Kripke. \\
 9 & 29/mai & Interpretação de IPL na lógica modal S4. Interpretação de S4 em topologias. \\
10 & 05/jun & Categorias. Set e ordens parciais como categorias. Terminais, iniciais, produtos e coprodutos. \\
11 & 12/jun & Dualidade. Unicidade módulo isomorfismo. Funtores. Transformações naturais. \\
12 & 19/jun & Adjunções e exponenciais. Categorias Cartesianas Fechadas. \\
13 & 26/jun & $λ$-cálculo em Categorias Cartesianas Fechadas. Semânticas Categóricas. \\
14 & 03/jul & Introdução ao Lua. Introdução ao Lisp. \\
15 & 10/jul & Implementação de um mini-Lisp. \\
16 & 17/jul & Eager evaluation e lazy evaluation. Implementação de thunks e lazy evaluation. \\
\end{longtable}

O cronograma acima é só um planejamento inicial - ele será ajustado
durante o curso. O cronograma real com o que foi executado em cada
aula poderá ser consultado na página do curso.




\section{Critério de aprovação}

A nota de cada aluno será dada de acordo com a sua participação em
aula.


\section{Bibliografia básica}

Paul Blain Levy: {\it Typed $λ$-calculus: course notes}. Disponível
em: \url{https://www.cs.bham.ac.uk/~pbl/mgsall.pdf}.

Peter Selinger: {\it Lecture Notes on the Lambda Calculus}. Disponível
em: \url{https://arxiv.org/pdf/0804.3434.pdf}.

Tom Leinster: {\it Basic Category Theory}. Disponível em:
\url{https://arxiv.org/pdf/1612.09375.pdf}.

Eduardo Ochs: {\it Planar Heyting Algebras for Children}. Disponível
em: \url{http://anggtwu.net/LATEX/2017planar-has-1.pdf}.

Eduardo Ochs: {\it On the Missing Diagrams in Category Theory
  (First-Person Version)}. Disponível em:
\url{http://anggtwu.net/LATEX/2022on-the-missing.pdf}.




\section{Página do curso}

Todo o material do curso, inclusive as fotos dos quadros, será posto
na página do curso, cujo link é:

\url{http://http://anggtwu.net/2023.1-LA.html}




\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "laplc"
% End: