On Thu, 2 Dec 2010, Petr Pudlak wrote:
Hi,
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
literature.
Voevodsky talks about the category of contexts in
<http://www.mefeedia.com/watch/31778282>, which I understand is described
in more detail in "Semantics of type theory : correctness, completeness,
and independence results" by Thomas Streicher.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
