Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2009-planodetrabalho.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg                 ".zshrc" "makebbl")
% (find-LATEX "catsem.bib")
% (find-LATEX "filters.bib")
% (defun b () (interactive) (find-zsh "makebbl 2009-planodetrabalho.bbl catsem,filters"))
% (defun b () (interactive) (find-zsh "bibtex  2009-planodetrabalho"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-planodetrabalho.tex && latex    2009-planodetrabalho.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-planodetrabalho.tex && pdflatex 2009-planodetrabalho.tex"))
% (defun d () (interactive) (find-dvipage "~/LATEX/2009-planodetrabalho.dvi"))
% (eev "cd ~/LATEX/ && Scp 2009-planodetrabalho.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2009-planodetrabalho.dvi")
% (find-pspage  "~/LATEX/2009-planodetrabalho.pdf")
% (find-pspage  "~/LATEX/2009-planodetrabalho.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi && ps2pdf 2009-planodetrabalho.ps 2009-planodetrabalho.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-sh0  "cd ~/LATEX/ && dvired -D 600 -P pk -o 2009-planodetrabalho.ps 2009-planodetrabalho.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009-planodetrabalho.pdf" (ee-twupfile "LATEX/2009-planodetrabalho.pdf") 'over)
% (ee-cp "~/LATEX/2009-planodetrabalho.pdf" (ee-twusfile "LATEX/2009-planodetrabalho.pdf") 'over)

% «.bibliography»	(to "bibliography")



\documentclass[a4paper,12pt]{article}

\usepackage[brazil]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amssymb,amsmath,amsthm}
\usepackage{babelbib}
\usepackage{url}

\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")


\newcommand{\hoje}{29 de julho de 2009}

\title{Plano de Trabalho}

\author{%
  Prof.\ Eduardo Nahum Ochs\\
  Ciência da Computação\\
  PURO -- Pólo Universitário de Rio das Ostras\\
  UFF -- Universidade Federal Fluminense%
}

\date{\hoje}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 
\begin{document}

\maketitle


\section{Apresentação}

  Este documento apresenta o plano de trabalho do professor Eduardo
  Nahum Ochs, matrícula SIAPE 1669224, em conformidade com a resolução
  219/2005 do Conselho de Ensino e Pesquisa da UFF.

  Ele está escrito um primeira pessoa; ao invés de escrever ``o
  professor Eduardo Ochs'', ``o professor'', etc., escreverei sempre
  ``eu''.

% {\sl Como em alguns pontos --- principalmente na descrição do
% projeto de pesquisa --- este documento precisa expôr impressões
% sobre vários caminhos possíveis e os motivos que provavelmente
% levarão à escolha de um (ou alguns) dentre estes caminhos, ele será
% escrito em primeira pessoa. Ao invés de escrever ``o professor
% Eduardo Ochs'', ``o professor'', etc, vou escrever sempre ``eu'' ---
% é muito mais natural e fluente expressar graus de certeza num texto
% em primeira pessoa que num texto em terceira.}

% A Seção~\ref{pesq} discute as atividades de pesquisa que o professor
% pretende conduzir; a Seção~\ref{ens} apresenta as propostas do
% professor relativas ao ensino; a Seção~\ref{ext} expõe os planos do
% professor na área de extensão.

\bsk

  A Seção~\ref{pesq} discute as atividades de pesquisa que pretendo
  conduzir; a Seção~\ref{ens} apresenta minhas propostas de atividades
  em ensino; a Seção~\ref{ext} expõe meus planos na área de extensão.

% (find-books "__cats/__cats.el" "maclane")
% (find-books "__logic/__logic.el" "typetheory")
% (find-LATEX "catsem.bib" "bib-LambekScott")


\section{Pesquisa}
\label{pesq}

  \subsection{Projeto de Pesquisa}

    Pretendo cadastrar um projeto intitulado ``Downcasing types:
    provas puramente sintáticas, a projeção de provas `reais' no
    `mundo sintático' e levantamentos de provas do `mundo sintático'
    para o `mundo real'\,'', que deve abarcar minhas principais
    atividades de pesquisa nos 2 primeiros anos de meu estágio
    probatório. Trata-se de um projeto nas áreas de Lógica
    (\cite{GLT})), Teoria de Categorias (\cite{CWM}, \cite{Awodey}),
    Teorias de Tipos (\cite{Kamareddine}), Semântica Categórica para
    Teorias de Tipos (\cite{Jacobs}), (formalização de) Raciocínio
    Diagramático (\cite{Kromer}, \cite{Jamnik}) e Assistentes de
    Provas (\cite{Automath}, \cite{BertotCasteran}), com aplicações à
    Teoria de Toposes (\cite{McLarty}, \cite{Johnstone},
    \cite{Elephant1}), à Análise Não-Standard (\cite{Robinson66}) e à
    Geometria Diferencial Sintética (\cite{Kock77}, \cite{Bell98}
    \cite{Antipodes}).

\bsk

    Meu projeto de pesquisa -- ``Downcasing Types'' --- é uma
    continuação da minha pesquisa de mestrado e doutorado, e que
    continuei desenvolvendo no período em que trabalhei fora do mundo
    acadêmico (2004-2008).

    Devido a particularidades da área de Teoria de Categorias (veja
    \cite{Kromer}) muitos resultados sobre Categorias são
    conceitualmente importantes, mas só se tornam publicáveis quando
    são usados para provar teoremas novos não-triviais. Só em 2008 eu
    consegui completar todos os detalhes de um primeiro resultado
    realmente não-trivial: um método para traduzir contas com
    infinitesimais --- feitas num fragmento da Análise Não-Standard
    --- para ``contas standard'' em termos de continuidade e limites,
    e submeti uma versão preliminar de um artigo (veja
    \url{http://angg.twu.net/math-b.html}) para discussão na mailing
    list internacional de Teoria de Categorias. A discussão que
    resultou disto me levou a produzir material introdutório sobre
    feixes e sobre lógica em grafos (veja a URL acima), usando as
    técnicas de ``downcasing types'' para obter um ``modelo
    arquetipal'' no qual todas as idéias ficassem claras, e a partir
    do qual pudéssemos produzir provas para casos particulares
    específicos que pudessem ser ``levantadas'' para o caso geral. Em
    2008 e no início de 2009 apresentei parte destas idéias em
    seminários na UFF de Niterói, no PURO-UFF, no IMPA e na PUC-Rio;
    em cada uma destas instituições os pesquisadores locais se
    interessavam mais por partes diferentes do que eu expunha, e todos
    me falavam que certos teoremas de Teoria de Categorias, Toposes e
    Feixes, que os livros dão a entender que são básicos, são
    praticamente desconhecidos por aqui; no máximo algumas poucas
    pessoas ouviram falar deles, mas ninguém nestas instituições tem
    uma boa intuição a respeito do que estes teoremas ``realmente''
    querem dizer... mesmo os livros tecnicamente mais acessíveis da
    \'area parecem ser dirigidos principalmente a pessoas que têm de
    algum modo acesso à ``cultura oral'' de Teoria de Categorias e
    Teoria de Toposes --- o que não é o nosso caso! --- e este meu
    trabalho sobre ``provas arquetipais'' para teoria de Feixes,
    segundo as pessoas com quem discuti, seria extremamente
    bem-vindo...

    {\sl Ainda não é claro para mim como esta parte da pesquisa} ---
    as provas arquetipais para os fatos básicos de teorias de feixes,
    e sobre lógica em feixes --- {\sl deva ser publicada;} se como
    material didático sobre um assunto que é relativamente avançado,
    ou como uma aplicação (num certo sentido trivial; será que aí ela
    teria que aparecer como um exemplo, brevemente, num artigo mais
    técnico?) da técnica geral de ``downcasing types'', ou se ela deve
    ser formalizada até os últimos detalhes e implementada num
    assistente de prova (como em \cite{BertotCasteran} e
    \cite{Automath})... e várias outras partes da pesquisa estão na
    mesma situação: os ``downcasings'' dos fatos básicos sobre mônadas
    (\cite{Schalk}), os para uma categoria na qual podemos fazer
    cálculo com infinitesimais nilpotentes (\cite{Kock77}), os para o
    chamado ``cálculo de frações'' numa categoria e para a
    interpretação categórica das ``ultrapotências'' usadas em Análise
    Não-Standard (\cite{Johnstone}, \cite{Fritz}), os para Categorias
    Abelianas (\cite{CWM}), e os para Categorias Diferenciais
    (\cite{SeelyDiff}, \cite{SeelyCartDiff}).

\bsk

    Apesar das dificuldades para publicar sobre determinados assuntos,
    que descrevi acima, os primeiros passos para começar a publicar a
    minha pesquisa estão definidos. Devo terminar no segundo semestre
    de 2009 um artigo sobre o método de ``downcasing types'', com pelo
    menos as seguintes aplicações: categorias com produtos finitos,
    Categorias Cartesianas Fechadas (\cite{LambekScott}) e
    Hiperdoutrinas (\cite{LawvereAdjFo}, \cite{SeelyBeck},
    \cite{Jacobs}). Em 2010 devo terminar artigos sobre downcasings
    para categorias localmente cartesianas fechadas (\cite{SeelyLCCC},
    \cite{Jacobs}), categorias nas quais se pode interpretar
    $\lambda$-cálculo polimórfico (\cite{SeelyPLC}, \cite{Jacobs}), e
    toposes (\cite{McLarty}), mas ainda não sei se estes assuntos
    podem ser desmembrados em dois ou três artigos ou se devem ficam
    num só; e depois disto vão vir os downcasings para feixes,
    categorias de frações, ultrapotências, e para uma categoria
    descrita em \cite{Kock77}, com infinitesimais nilpotentes (ver
    também \cite{MoeRey}, \cite{Kock81}, \cite{BellSIA}). {\sl Um
      cronograma detalhado será dado no projeto de pesquisa.}



% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008sheaves.tex")


%   Ao longo da realização do projeto, o professor pretende interagir
%   com o Laboratório de Tecnologias e Métodos Formais (TecMF) da
%   PUC-Rio, criando um vínculo interinstitucional que certamente será
%   proveitoso para o PURO e para a UFF.

  \subsection{Iniciação Científica}

    Ao longo de 2010 e 2011 pretendo orientar um ou mais alunos de
    bolsa acadêmica e/ou de iniciação científica em atividades
    relacionadas ao projeto de pesquisa descrito acima.

  \subsection{Desenvolvimento e Documentação de Software}
  \label{software}

    Pretendo terminar de documentar um programa que comecei a
    desenvolver durante o meu mestrado
    (\url{http://angg.twu.net/dednat4.html}), que facilita tarefas
    como bater árvores de dedução em diagramas categóricos em \LaTeX.
    Alguns alunos de graduação do PURO já se interessaram em usá-lo
    para o tipo de árvores de dedução que eles vêem nas matérias de
    Matemática Discreta e Lógica, e eu e o professor Fernando Náufel
    do Amaral estamos pensando em modificar este programa para que ele
    possa gerar diagramas 2D a partir de outros tipos de ``input'' que
    não os atuais.

  \subsection{Instalação de Software}

    Para tornar as ferramentas e assuntos de pesquisa do LLaRC mas
    acessíveis para os alunos do PURO pretendo conseguir que sejam
    instalados os seguintes programas e sistemas nos computadores do
    Pólo (inclusive os do laboratório dos alunos de graduação):

    \begin{itemize}
    
      \item Emacs   (\url{http://en.wikipedia.org/wiki/Emacs}),
      \item Eev     (\url{http://angg.twu.net/emacs.html#short-eev-tutorial}),
      \item \LaTeX  (\url{http://en.wikipedia.org/wiki/LaTeX}),
      \item Lua     (\url{http://www.lua.org/}),
      \item Maxima  (\url{http://en.wikipedia.org/wiki/Maxima_(software)}),
      \item GnuPlot (\url{http://en.wikipedia.org/wiki/Gnuplot}),
      \item Dednat4 (\url{http://angg.twu.net/dednat4.html}).
      \item Hugs    (\url{http://en.wikipedia.org/wiki/Hugs}).
      \item Ruby    (\url{http://en.wikipedia.org/wiki/Ruby_(programming_language)}).
      \item Python  (\url{http://en.wikipedia.org/wiki/Python_(programming_language)}).
      \item Tcl/Tk  (\url{http://en.wikipedia.org/wiki/Tcl}),
      \item OCaml   (\url{http://en.wikipedia.org/wiki/Objective_Caml}).
      \item Coq     (\url{http://en.wikipedia.org/wiki/Coq}),

    \end{itemize}

    Obs: todos os programas acimas são não só gratuitos para
    instalação e uso como são ``livres'' --- suas licenças permitem
    cópia e modificação pelos usuários.

% {\sl Assistentes de provas: Coq e Isabelle; interpretadores para
%   diversas linguagens: Hugs; Ruby; Python; Tcl/Tk; ML; beanshell}

%      \item Os sistemas \TeX\ e \LaTeX\ de editoração eletrônica de
%        documentos técnicos e científicos
%        (\url{http://www.latex-project.org/});
    
  \subsection{Seminários}

    Pretendo apresentar seminários regulares no LLaRC (o Laboratório
    de Lógica e Representação do Conhecimento do PURO-UFF), e
    esporádicos na UFF de Niterói, na PUC-Rio e no IMPA sobre temas
    avançados e básicos relacionados ao meu projeto de pesquisa, dando
    continuidade aos contatos acadêmicos que estabeleci antes da minha
    contratação pelo PURO.

\section{Ensino}
\label{ens}

  \subsection{Disciplinas}

    Estou apto a ministrar disciplinas diversas relacionadas aos
    seguintes conteúdos:

    \begin{itemize}

      \item Cálculo I, II, III, IV;

      \item Equações Diferenciais;

      \item Álgebra Linear;

      \item Matemática Discreta;

      \item Análise Combinatória;

      \item Lógica;

      \item Teoria de Categorias;

      \item Teoria dos Números.

      % \item Linguagens de programação;

    \end{itemize}

% (find-LATEX "catsem.bib" "Bootstrapping")

    Além de disciplinas obrigatórias, pretendo oferecer disciplinas
    optativas e orientar trabalhos de conclusão de curso nas áreas de
    Lógica, Semântica, ``Domain-Specific Languages''
    (\cite{LittleLanguages}, \cite{Bootstrapping}) e Linguagens
    Funcionais, bem como obter credenciamento para atuar nos programas
    de pós-graduação dos departamentos de Matemática e Ciência da
    Computação de Niterói, ministrando disciplinas ligadas às minhas
    \'areas de interesse e orientando dissertações e teses.

  \subsection{Projeto de Ensino}
  \label{projens}

  Pretendo ministrar, começando ainda em 2009, alguns workshops sobre
  como usar diversos programas interativos --- essencialmente todos os
  da seção \ref{software} --- a partir do Emacs, guardando os logs num
  formato que seja útil para as pessoas que vierem depois (veja
  \url{http://angg.twu.net/eev-article.html}). Aos poucos vou tentar
  descobrir como transformar estes workshops num projeto de ensino com
  existência oficial, com conteúdos e objetivos bem-definidos,
  cronogramas, etc.

%    {\sl [Uma vez que as instalações dos programas nos laboratórios de
%        informática do PURO tenham sido concluídas pretendo
%        implementar um projeto de ensino relacionado a linguagens
%        funcionais interativas (em especial Lua), interfaces textuais
%        programáveis (Emacs e Eev), e ferramentas para geração de
%        gráficos que possam ser controladas por interfaces textuais
%        programáveis (Gnuplot).]}

\section{Extensão}
\label{ext}

  \subsection{Projeto de Extensão}

    O projeto de ensino da seção \ref{projens} é uma espécie de
    continuação de um projeto de software livre que eu tenho desde o
    fim da década de 90, e que interessa à comunidade de Software
    Livre em geral.

    Pretendo submeter à PROEX em 2010 um projeto de extensão
    relacionado a isto.

%    {\sl [Ainda em 2006, o professor pretende apresentar à PROEX um
%        projeto para o desenvolvimento e implementação, no PURO, de
%        cursos de extensão (básicos e avançados) sobre os sistemas
%        \TeX\ e \LaTeX\ de editoração eletrônica de documentos
%        técnicos e científicos (\url{http://www.latex-project.org/}).
%        O público-alvo destes cursos inclui alunos e professores dos
%        diversos cursos do PURO, bem como profissionais de nível
%        técnico ou superior, que tenham interesse em produzir
%        documentos técnicos e científicos (artigos, apostilas,
%        manuais, etc.) de alta qualidade tipográfica. Esta atividade
%        deverá incluir a participação de alunos bolsistas de
%        extensão.]}




\vskip 2cm

\noindent Rio das Ostras, \hoje\

\vskip 2cm

\noindent Prof.\ Eduardo Nahum Ochs

\noindent Matr.\ SIAPE 1669224


\newpage


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips  -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvips  -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

% {\myttchars
% % \footnotesize
% \normalsize
% \begin{verbatim}
% Software
% ========
%   Dois fronts que se entrecruzam:
%   Dednat4
%   Forth/Lua --> Isabelle etc.
%   A relação com o eev é um pouco mais distante.
% 
% Novos teoremas
% ==============
%   Infinitesimais naturais
%   Formalização da idéia de levantamento?
%   Traduções de contascom infinitesimais
%   ND for PLC
%   ND for LCCCs
% 
% Distant goals
% =============
%   Realizability
%   Parametricity
%   Differential Categories
%   Property-like structures
%   Calculus of variations
%   Relate to Freyd's book
% 
% Landmarks
% =========
%   Downcasing hyperdoctines
%   Formalizar liftings & archetypes
%   Mundo sintático e mundo real
% \end{verbatim}
% }
% 
% \newpage
% 
% {\myttchars
% % \footnotesize
% \normalsize
% \begin{verbatim}
% Representações/traduções/impls/provas arquetipais
% =================================================
%   Yoneda
%   Mônadas
%   Tradução de boa parte do CWM
%   Sheaves
%   Geometric morphisms
%   Reyes/Zolfaghari
%   \eps^2=0
%   Filter-powers
%   Abelian categories
%   
% CFPs -> CCCs -> Hyps -> PLC -> Hask
%                      \-> LCCCs -> Toposes
% 
% Colaborações prováveis, engatilhadas
% ====================================
%   Fnaufel
%   Mrac Simpson
% 
% Colaborações não-óbvias
% =======================
%   Valéria de Paiva
%   Seely
%   Petrúcio/Renata
%   Veloso?
% 
% Etc:
% ====
%   Jibladze
%   Sheaves as categories of fractions 
% \end{verbatim}
% }
 
% «bibliography»  (to ".bibliography")
% (find-es "tex" "makebbl" "nocite{*}")
%   Occasionally the bibliography is to include publications that were
% not referenced in the text. These may be added with the command
%   \nocite{key}
% given anywhere within the main document. It produces no text at all
% but simply informs BIBTEX that this reference is also to be put into
% the bibliography. With \nocite{*}, every entry in all the databases
% will be included, something that is useful when producing a list of
% all entries and their keys.

% \nocite{*}

% (find-LATEX "catsem.bib" "test")
% (find-LATEX "filters.bib")
% (find-zsh "makebbl 2009-planodetrabalho.bbl catsem,filters")
% (find-es "tex" "makebbl")
% \bibliographystyle{alpha}
\bibliography{catsem,filters}
\bibliographystyle{alpha}

\end{document}



% (find-eapropos "coding")
% coding:           latin-1-unix


% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: