[Agda] Mendori

[jeff polakow]

Hello,

> What are dependently typed records?  What do they give you beyond
> sig types, and single constructor data types?
>
There is a paper in TLCA'03 by Coquand, Pollack, and Takeyama called "A
Logical Framework with Dependently Typed Records" which gives a semantic
foundation and typechecking algorithm, which is the starting point for
Mendori.

One of the main reasons for exploring dependently typed records is to reason
about first class modules; the type system of Mendori includes opaque
and manifest fields in addition to subtyping.

Jeff Polakow
JST CREST researcher
AIST Research Center for Verification and Semantics
email: j-polakow at aist.go.jp