[Haskell-cafe] Categorical description of systems with dependent types

Petr Pudlak deb at pudlak.name
Thu Dec 2 16:13:32 CET 2010


recently, I was studying how cartesian closed categories can be used to 
describe typed functional languages. Types are objects and morphisms are 
functions from one type to another.

Since I'm also interested in systems with dependent types, I wonder if 
there is a categorical description of such systems. The problem (as I 
see it) is that the codomain of a function depends on a value passed to 
the function.

I'd happy if someone could give me some pointers to some papers or other 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20101202/73967519/attachment.pgp>

More information about the Haskell-Cafe mailing list