## Eduardo Ochs - Academic Research - Categorical Semantics, Downcasing Types, Skeletons of Proofs, and a bit of Non-Standard AnalysisQuick index:
- IPL For Children and Meta-Children, or: How Archetypal Are ZHAs?
- Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2017)
- Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2015)
- Logic and Categories, or: Heyting Algebras for Children (2015)
- Sheaves for children (2014)
- Sheaves on Finite DAGs may be Archetypal (2011)
- Internal Diagrams in Category Theory (2010)
- Downcasing Types (at UniLog'2010)
- Natural infinitesimals in filter-powers (2008)
- Sheaves for Non-Categorists (2008)
- Seminar on downcasing types (nov/2007)
- General links
- PhD and post-PhD research
- MsC Thesis and related things
- Typesetting categorical diagrams in LaTeX
## IPL For Children and Meta-Children, or: How Archetypal Are ZHAs?This is a 20-minute talk that I will give in the
EBL2017.
## Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2017)Finite planar Heyting Algebras ("ZHA"s) are very good tools for teaching Heyting Algebras and Intuitionistic Propositional Logic to "children"; "children" here means "people without mathematical maturity", in the sense that they are not able to understand structures that are too abstract straight away, they need particular cases first. These notes cover roughly the same material as the ones below, that
have the same title but a "2015" at the end, but in a self-contained
way. Everything has been rewritten, and some of the sections have been
tested on real "children" (sophomore CS students); they found the text
of
The PDF (current version: 2017mar07).
## Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2015)
Seminar notes, with lots of figures (all drawn with Dednat6).
## Logic and Categories, or: Heyting Algebras for Children (2015)A tutorial presented at the UniLog 2015 conference (Istanbul), 20-22/jun/2015.
## Sheaves for children (2014)A 20-minute talk - here are its slides - presented at the XIV EBL, on 2014apr09. Its abstract:
The second - and much longer - version of this talk (at the Seminário Carioca de
Lógica, 2014may19, 15:00, IFCS) had these
slides and these
handouts, and was meant for much younger "children". The focus this
time was a visual characterization of the subsets of N ## Sheaves on Finite DAGs may be Archetypal (2011)Can the ideas of my article about "internal diagrams" be used to present the basic concepts of toposes and sheaves starting from simple, "archetypal" examples? I believe so, but this is still a work in progress! Here are 7 pages of ...and here are some slightly older notes - I submitted them, in a admittedly incomplete form, to the XVI EBL, with this abstract - and then I did a bad job at presenting them; here are the slides, they cover only the first ideas =(. For the sake of completeness, here are some handwritten diagrams describing Kan extensions in an (hopefully) archetypal case, motivated by discussions with G.F. Lima: 1200dpi djvu, 600dpi djvu, 600dpi pdf. ## Internal Diagrams in Category Theory (2010)A paper submitted to
The paper was produced from the material that I created for the talk below. The slides covers much more ground, but the paper explains the ideas much more clearly. The revised version (2013), that has more sections and more words in the title: "Internal Diagrams and Archetypal Reasoning in Category Theory" (if you prefer a .dvi, it needs this .eps). The original version (just "Internal Diagrams in Category Theory", 2010) is here. (2013) Internal Diagrams and
Archetypal Reasoning in Category Theory
## Downcasing Types (at UniLog'2010)I gave a talk about Downcasing Types at the special session on Categorical Logic of UNILOG'2010, on 2010apr22. Very few people attended - because the volcanic ashes many people could not fly to Portugal, and from all these programmed talks only these ended up happening. The abstract was:
(A longer version of the abstract: pdf.) First official release of the slides (2010jun21, 100 pages): pdf. Latest version of the slides (109 pages): dvi, pdf. Some related posts at cat-dist:## Natural infinitesimals in filter-powers (2008)"Purely calculational proofs" involving infinitesimals can be
"lifted" from the non-standard universe (an ultrapower) to the
"semi-standard universe" (a filter-power) through the quotient
Set
Preliminary version (2008jul13), including the message to the mailing list: pdf, dvi, source. A (long-ish) abstract for a presentation intended for undergrads:
pdf,
source.
(News: Reinhard Boerger pointed me to later (post-1958) work by Laugwitz and Schmieden, and I got a copy of the "Reuniting the Antipodes" book; my current impression is that my result is not as trivial as I was afraid it could be. Homework-in-progress: several cleanups on the preliminary version above, and I'm trying - harder - to understand Moerdijk and Palmgren's sheaf models.) Note (2010): ## Sheaves for Non-Categorists (2008)This is another presentation that - Here's an htmlized version of the abstract:
## 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: - 1. Downcasing Sets
- 2. Downcasing Type Systems
- 3. Downcasing the Beck-Chevalley Condition
- 4. Downcasing the Structure of a Topos
- 5. Downcasing Comprehension Categories
- 6. Notes about Hyperdoctrines
- 7. Notes about Sheaves
- 8. Downcasing ring objects of line type (as in Kock77; for SDG)
- 9. Notes about monads (and *-autonomous and differential categories)
- 10. Notes about the notation in several papers
- 11. Notes about the notation in Kock & Mikkelsen's paper on ultrapowers
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- http://ncatlab.org/nlab/show/HomePage
- The Collection of Computer Science Bibliographies
- CiteSeer (broken?)
- CiteSeerX
- DBLP
- http://www.tac.mta.ca/tac/
- http://www.mta.ca/~cat-dist/
- http://news.gmane.org/gmane.science.mathematics.categories
- Cahiers de Topologie et Géométrie Différentielle Catégoriques
- http://arxiv.org/list/math.CT/recent
- http://arxiv.org/help/
- Frank Atanassow's list of online Programming Language Theory texts
- http://arxiv.org/
- ASL journals: JSL and BSL
- http://www.cs.nyu.edu/pipermail/fom/
- http://www.informatik.uni-trier.de/~ley/db/journals/
- Le petit Nicolas en thèse
- The Brazilian mailing list on logic, and some notes on one of its most vocal members.
- http://math.ucr.edu/home/baez/TWF.html
- http://www.ams.org/mathweb/mi-books.html
- http://onlinebooks.library.upenn.edu/webbin/book/callover?key=Q
## Some articles and books that I'm reading:- Blute, Cockett & Seely: Differential Categories (2005)
- Notes by Andrea Schalk: monads, cat. models for LL, games
- Notes by Harold Simmons, esp. this one about sheaves on omega-sets
- Fiore, Leinster: Objects of Categories as Complex Numbers (2002)
- Leinster: A proof that sheaves do not belong to algebraic geometry (2007)
- J. L. Bell: A Primer of Infinitesimal Analysis (1998)
- Eisenbud & Harris: The Geometry of Schemes
- Cockett & Seely: Polarized Category Theory, Modules, and Game Semantics (2004)
- M. P. Jones:
- Robin Milner: A Theory of Type Polymorphism in Programming (1978)
- John Allen: Anatomy of Lisp (1978)
- Bart Jacobs: Categorical Logic and Type Theory
- Papers about Charity:
## Category Theory (in general):- Barr/Wells: Toposes, Triples, and Theories (1985).
- Phil Scott: Some Aspects of Categories in Computer Science (1998/2000; a chapter of the "Handbook of Algebra")
- Andy Pitts: Categorical Logic (2001) (CS entry)
- Noson Yanofsky's paper about diagonal arguments (2003)
## Fibrations:- Thomas Streicher's notes on Fibered Categories à là Jean Bénabou (1999)
- Wesley Phoa: An Introduction to Fibrations, Topos Theory, the Effective Topos and Modest Sets
## Monads:- Notes by Andrea Schalk
- Blute/Scott: Category Theory for Linear Logicians
- Jon Beck's thesis and TTT, from TAC reprints
## Sheaves:## Type Theory (mainly the Calculus of Constructions):- Herman Geuvers's...
- Barendregt: Lambda Calculi with Types (1992) (CS entry)
- Zhaohui Luo's PhD thesis: "An Extended Calculus of Constructions" (1990).
- W.M.Farmer: The Seven Virtues of Simple Type Theory (2003)
- Jonathan Seldin's homepage
- Thierry Coquand's homepage
- Barbanera/Berardi: Proof-Irrelevance out of Excluded Middle and Choice in the Calculus of Constructions
- Milly Maietti's home page
- Martin Hofmann: Extensional concepts in intensional type theory (PhD thesis, 1995), Syntax and Semantics of Dependent Types (1997)
- LCCCs:
- Nordström/Petersson/Smith: Martin-Löf's Type Theory
- Mark P. Jones: First Class Polymorphism with Type Inference (1997)
## Parametricity:## Non-standard Analysis, SDG and friends:- A page with many links on Non-Standard Analysis
- William Lawvere:
- Jonas Eliasson's thesis; he makes reference to some papers by Erik Palmgren that are not on-line.
- Thomas Ehrhard: The Differential Lambda-Calculus (2001).
- Anders Kock:
- A simple axiomatics for differentiation (1977)
- Synthetic Differential Geometry (1981/2006)
- Topos-theoretic factorization of non-standard extensions (1974, witk Mikkelsen; SLNM 369)
- Aspects of Fractional Exponent Functors (1999, with G. Reyes)
- Fractional Exponent Functors and Categories of Differential Equations (1998, with G. Reyes)
- Carsten Butz: The filter construction revisited
## Natural Deduction:## Grothendieck:- Biographical article in Notices of the AMS, parts 1 and 2 (2004)
- McLarty: The Rising Sea: Grothendieck on simplicity and generality (2003)
- http://kolmogorov.unex.es/~navarro/res/
- http://mapage.noos.fr/recoltesetsemailles/TdM.htm
## Etc (unclassified):- http://alessio.guglielmi.name/res/cos/PN/index.html
- http://www.phil.cmu.edu/projects/ast/
- http://www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf
- http://www.mat.ufmg.br/~elaine/
- http://www.fields.utoronto.ca/programs/scientific/06-07/homotopy/courses/
Links to the home pages of some category theorists (and a few type theorists): Abadi, Abramsky, Aczel, Adamek, Altenkirch, Aspinall, Atanassow, Avigad, Awodey, Baez, Barendregt, Barr, Bauer, Beeson, Bell, Berardi, Berg, Birkedal, Blass, Blute, Brown, Bunge, Butz, Caccamo, Cockett, Coquand, Crosilla, Dawson, DePaiva, Diaconescu, Dosen, Dybjer, Egger, Ehrhard, Escardo, Fiore, Funk, Gaucher, Geuvers, Girard, Grandis, Gurevich, Hasegawa, Hermida, Hofmann, Hofstra, Honsell, Hyland, Jacobs, Jardine, Jibladze, Joyal, Kock, Koslowski, Lack, Lamarche, Lambek, Laurent, Lawvere, Leinster, Levy, Longo, Luo, MPJones, Maietti, Mairson, Makkai, Marcos, McLarty, Maltsiniotis, Milner, Mislove; Moerdijk, Moggi, Nelson, Negri, Niefield, Palmgren, Pare, Pastro, Pavlovic, Petric, Phoa, Pierce, Pitts, Plotkin, Porter, Pratt, Pronk, Queiroz, Regnier, Reynolds, Rosebrugh, Rosolini, Sambin, Scedrov, Schalk, Schuster, Scott, ScottD, Seely, Seldin, Selinger, Simmons, Simpson, Spitters, Street, Streicher, Taylor, Tholen, VanOosten, Vickers, Wadler, Weirich, Wells, Wiedijk, Winskel, Wood, Wraith, Yanofsky. ## PhD and post-PhD researchI 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
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. News (2010/2013): this paper has all the ideas from my PhD thesis, plus some! It fills all the gaps from the thesis, and it is quite well written =).
I also gave Slides for the longer talk (45 minutes, 26+3 pages): pdf, ps, dvi, source. Slides for the shorter talk (one week later, 15 minutes, 16+2 pages: pdf, ps, dvi, source.
Abstract (3 pages and a bit): pdf, ps, dvi, source. Slides (16 slides): pdf, ps, dvi+eps's, source.
The notes from which the slides were made: ps, dvi+eps's, source. ## MsC Thesis and related things
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: pdf, ps, dvi+eps's, source. My advisor at PUC: Nicolau Saldanha ## Typesetting categorical diagrams in LaTeXMy 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.
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 |