User loginNavigation |
archivesExamples of encodings in Pure Type SystemsI am toying with implementing a pure type system (formally described in section 5.2 of "Lambda Calcui with Types"). I've extended the specification to include sum type introduction, formation and elimination. I've written a few examples but I'm looking for a library of example encodings in (minimal) pure type systems. In particular, I'm looking to extend the PTS as little as possible but still want to be able to translate (from a higher level language) constructs such as abstract data types and pattern matching. I read somewhere, maybe something authored by Conor McBride, that some of this is possible, but I lost that reference. |
Browse archivesActive forum topics |
Recent comments
16 weeks 2 days ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 11 hours ago
51 weeks 4 days ago
51 weeks 4 days ago