Quick
index
main
eev
maths
blogme
dednat4
littlelangs
emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
debian-rj
w32/AIX
politics
personal
heroes
irc
contact
☿

Eduardo Ochs - Academic Research - Categorical Semantics, Downcasing Types, Skeletons of Proofs, and a bit of Non-Standard Analysis

I'm currently living in a strange limbo between the academic world and the real world.

Quick index:

Seminar on downcasing types (nov/2007)

If you are going to attend my seminars at PUC at November/2007 and want to take a peek at my notes (they are very incomplete at the moment, it goes without saying), they have just been split into several parts:

I'm planning to finish the part on downcasing BCC soon, and to typeset it using dednat4, and to include its slides in the dednat4 package as examples. I'm also planning to complete a few pendencies on dednat4 soon, and to release it "officially". The notes of downcasing BCC should be readable (when completed, of course) by anyone with some background in Category Theory independently of the other parts.

Bad news (?), dec/2007: the seminars will not happen - instead, I got a job at São Paulo, on computer stuff. I'll keep working on maths and on my personal free software projects in my spare time. If you find any of these things interesting, and want to discuss or to encourage me to finish something, get in touch!

2008: I am giving a series of seminars at UFF to try to organize my ideas about downcasing types... here are links to some of TeXed slides (they are very preliminary, too. Should I be embarassed to provide links to these things? Well...):

General links

Some articles and books that I'm reading:

(The next sections are links to online texts.)

Category Theory (in general):

Fibrations:

Monads:

Sheaves:

Type Theory (mainly the Calculus of Constructions):

Parametricity:

Non-standard Analysis, SDG and friends:

Natural Deduction:

Grothendieck:

Etc (unclassified):

Links to the home pages of some category theorists (and a few type theorists): Abadi, Abramsky, Aczel, Adamek, Altenkirch, Atanassow, Awodey, Baez, Barr, Bauer, Beeson, Bell, Berardi, Berg, Birkedal, Blass, Blute, Bunge, Butz, Caccamo, Cockett, Coquand, Dawson, DePaiva, Dybjer, Egger, Ehrhard, Escardo, Fiore, Funk, Gaucher, Geuvers, Girard, Grandis, Hermida, Hofmann, Honsell, Hyland, Jacobs, Jardine, Jibladze, Joyal, Kock, Koslowski, Lack, Lambek, Laurent, Lawvere, Leinster, Levy, Luo, MPJones, Maietti, Mairson, Makkai, Marcos, McLarty, Maltsiniotis, Milner, Moerdijk, Moggi, Nelson, Negri, Niefield, Pare, Pastro, Pavlovic, Pitts, Plotkin, Pratt, Pronk, Regnier, Reynolds, Rosebrugh, Sambin, Scedrov, Schalk, Scott, ScottD, Seely, Seldin, Selinger, Simmons, Simpson, Street, Streicher, Taylor, Tholen, VanOosten, Vickers, Wadler, Weirich, Wells, Wiedijk, Winskel, Wood, Wraith, Yanofsky.

PhD and post-PhD research

I did both my MsC and my PhD (and also my graduation, by the way) at the Department of Mathematics at PUC-Rio. The Dept of Mathematics is a fantastic place - tiny, incredibly friendly, well-equipped, lots of research going on -, but (rant mode on) PUC-Rio is a private university, and most of the students from other departments were ultra-competitive rich kids who had never stepped out of the marble towers they live in. I used to find it very hard - very painful, even - to interact with them, and even to stand their looks, like if they were always trying to tag me as either a "winner" or a "loser", as if there weren't any other ways to live. Eeek! But these days are long gone now (rant mode off).

I spent the first eight months of 2002 at McGill University in Montreal, doing research for my PhD thesis there, working with Robert Seely... I was in a "Sandwich PhD" program (thanks CAPES!), which is something that lets us do part of the research abroad and then come back and finish (and defend) the thesis at our university of origin.

I defended my PhD thesis (with a few holes) in August, 2003 and presented the final version - filling out most of the gaps - in February, 2004. Then I spent most of 2004 teaching part-time in an university at the outskirts of Rio (the more realworldish job that I've ever had!), and also finishing a very important Free Software project that I've been working on since 1999 (GNU eev).

The thesis is in Portuguese and you don't want to see it - you want to see the slides that I'm working on (it's 2005mar12 as I write this), in which the method for interpreting diagrams and "lifting" them from Set to an arbitrary category with the adequate structure in explained in a really nice way. But if you are really anxious you can get in touch with me.

News (October 2005): I'm giving a series of talks about my PhD thesis at UFF (see http://www.uff.br/grupodelogica/). Expect slides soon and articles not so soon, but as soon as possible.

This is the abstract for a talk that I gave at the FMCS2002 in June 8, 2002.

Title: A System of Natural Deduction for Categories

We will present a logic (system DNC) whose terms represent categories, objects, morphisms, functors, natural transformations, sets, points, and functions, and whose rules of deduction represent certain constructive operations involving those entities. Derivation trees in this system only represent the "T-part" (for "terms" and "types") of the constructions, not the "P-part" ("proofs" and "propositions"): the rules that generate functors and natural transformations do not check that they obey the necessary equations. So, we can see derivations in this system either as constructions happening in a "syntactical world", that should be related to the "real world" in some way (maybe through meta-theorems that are yet to be found), or as being just "skeletons" of the real constructions, with the P-parts having been omitted for briefness.

Even though derivations in DNC tell only half of the story, they still have a certain charm: DNC terms represent "types", but a tree represents a construction of a lambda-calculus term; there's a Curry-Howard isomorphism going on, and a tree can be a visual help for understanding how the lambda-calculus term works -- how the data flows inside a given categorical construction. Also, if we are looking for a categorical entity of a certain "type" we can try to express it as a DNC term, and then look for a DNC "deduction" having it as its "conclusion"; the deduction will give us a T-part, and we will still have to go back to the standard language to supply a P-part, but at least the search has been broken in two parts...

The way to formalize DNC, and to provide a translation between terms in its "logic" and the usual notations for Category Theory, is based on the following idea. Take a derivation tree D in the Calculus of Constructions, and erase all the contexts and all the typings that appear in it; also erase all the deduction steps that now look redundant. Call the new tree D'. If the original derivation, D, obeys some mild conditions, then it is possible to reconstruct it -- modulo exchanges and unessential weakenings in the contexts -- from D', that is much shorter. The algorithm that does the reconstruction generates as a by-product a "dictionary" that tells the type and the "minimal context" for each term that appears in D'; by extending the language that the dictionary can deal with we get a way to translate DNC terms and trees -- and also, curiously, with a few tricks more, and with some minimal information to "bootstrap" the dictionary, categorical diagrams written in a DNC-like language.

I also gave a shorter version of that talk at the CMS Summer 2002 Meeting, in June 17.

Slides for the longer talk (45 minutes, 26+3 pages): ps, dvi, source.

Slides for the shorter talk (one week later, 15 minutes, 16+2 pages: ps, dvi, source.

Fact: all the essential details (i.e., the "T-part", as in the abstract above) of a certain construction of a categorical model of the Calculus of Constructions - and also of categorical models of several fragments of CC - can be expressed in (a few!) categorical diagrams using the DNC language. I'm currently (February/March 2005) preparing talks and articles about that.

An older talk about Natural Deduction for Categories. After using something like the DNC notation for years just because "it looked right", but without any good formal justification for it, in February 2001 I had the key idea: there were rules of both discharge and introduction for the "connectives" for functors and natural transformations. A few months after that (in July 5 2001, to be precise) I gave a talk about it at a meeting called Natural Deduction Rio 2001.

Abstract (3 pages and a bit): ps, dvi, source.

Slides (16 slides): ps, dvi+eps's, source.

Another talk, even older, about Natural Deduction for Categories. After finding the key idea that I mentioned above I arranged to give a (very informal) talk at the Centro de Lógica e Epistemologia at UNICAMP. It happened in April 25, 2001, and for it I had to assemble my personal notes into something that could be used as slides. The title was ""Set^C is a topos" has a syntactical proof".

The notes from which the slides were made: ps, dvi+eps's, source.

MsC Thesis and related things

My master's thesis: "Categorias, Filtros e Infinitesimais Naturais" (April, 1999). The thesis and the slides used in the defense are in Portuguese.

Thesis (7+116 pages): ps, pdf, dvi+eps's, source.

Slides (15 slides): ps, pdf, dvi+eps's, source.

The diagrams were made with diaglib and the deduction trees with dednat.icn.

A few months after the defense (in February 24, 2000, to be precise) I gave a talk at UFF about a kind of "Nonstandard Analysis with Filters", and about skeletons of proofs. Slides (12 slides plus one page), in Portuguese: ps, dvi+eps's, source.

My advisor at PUC: Nicolau Saldanha

Typesetting categorical diagrams in LaTeX

My PhD thesis included lots of hairy categorical diagrams, and I ended up writing a LaTeX preprocessor in Lua to help me typeset them. Currently (March 2005) I'm trying to pack that preprocessor and document it; its README is still horribly incomplete. The source code for the examples below is here.

if a functor R has a left adjont
then it preserves limits
The Beck-Chevalley map
in an LCCC
The Frobenius map
in an LCCC
Proving transitivity
in an EqFibration

Technical information: this page was made with blogme; the source is here. I access local copies of papers with the functions defined in my .emacs.papers. The diagrams were made by processing this file (oops, which?) with dednat4, then viewing the resulting dvi file with xdvi and taking screenshots with Xscreenshot-rect.