Blogs about: Type Theory
Featured Blog
The 2012 JAIST Spring School Part 2
This will be my final post on the JAIST spring school. If you have not already read my first post you can find it here. This post will summarize the third and forth days of the spring school. The fift… more →
Metatheorem
Why Not Lambda Encode Data?
— 8 comments
wrote 2 months ago: Datatypes are a conundrum for designers of type theories and advanced programming languages. For doi … more →
New Foundations
— 4 comments
wrote 2 months ago: It was around the beginning of my undergraduate studies when I became interested in foundations of m … more →
Introduction
— 9 comments
wrote 2 months ago: So I have finally set up my blog on various things that I am interested in and that are roughly rela … more →
The 2012 JAIST Spring School Part 2
wrote 2 months ago: This will be my final post on the JAIST spring school. If you have not already read my first post yo … more →
The 2012 JAIST Spring School Part 1
wrote 2 months ago: It has been a little while since my last post so I figured I would write a series of posts about my … more →
Random Inhabitation
— 2 comments
wrote 3 months ago: The semester is well underway here at The University of Iowa. I and the people I work with here are … more →
The Relationship between the LambdaMu-Calculus and the LambdaDelta-Calculus
wrote 5 months ago: As a part of my recent research on combinatorial proofs of the simply typed -Calculus I have been th … more →
A quick response to my question posed in my previous post
— 1 comment
wrote 6 months ago: In my previous post on Parigot’s -Calculus I did not understand the need for the first order q … more →
The Reflective Impulse
wrote 6 months ago: If the unexamined life is not worth living, how attractive then is the life of reflection, where in … more →
Notes on Parigot's Paper Introducing the Lambda-Mu-Calculus
wrote 6 months ago: Parigot defined the -calculus in his paper “The -Calculus: An Algorithmic Interpretation of Cl … more →
Implicit Type Promotion and Conversion
wrote 7 months ago: C introduced it and C++ mastered it. The hellish world of implicit conversion and type promotion. A … more →
Infinitary Logics
— 3 comments
wrote 7 months ago: In the comments of my previous post Updated: A Word on Consistency of Type Theories I had mentioned … more →
Updated: A Word on Consistency of Type Theories
— 14 comments
wrote 7 months ago: Okay. So last night I did some thinking and I have decided based on the comments from Chris and Vilh … more →
Why this blog?
wrote 10 months ago: Ever since getting exposed to type theory over the past year, I have been surprised over and over ag … more →
Types and Cells
— 5 comments
wrote 12 months ago: The doctrine of computational trinitarianism implies that there should be a categorial analogue of t … more →
Transformations as strict groupoids
— 6 comments
wrote 1 year ago: The distinguishing feature of higher-dimensional type theory is the concept of equivalence of the me … more →
Higher-Dimensional Type Theory
— 3 comments
wrote 1 year ago: Ideas have their time, and it’s not for us to choose when they arrive. But when they do, they … more →
More on abstract thinking and computer science
wrote 1 year ago: From FOM DIgest Vol 101, Issue 29, Tue, 24 May 2011 00:41:26 +0200, a post by Jeff Sarnat: As a com … more →
Topology/homotopy theory conferences in 2011
wrote 1 year ago: There are loads of conferences in topology this summer – here is a small selection. See AlgTop … more →
