|
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
|
3 <html> |
|
4 |
|
5 <head> |
|
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
7 <title>Codatatype Package</title> |
|
8 </head> |
|
9 |
|
10 <body> |
|
11 |
|
12 <h3><i>Codatatype</i>: A (co)datatype package based on bounded natural functors |
|
13 (BNFs)</h3> |
|
14 |
|
15 <p> |
|
16 The <i>Codatatype</i> package provides a fully modular framework for |
|
17 constructing inductive and coinductive datatypes in HOL, with support for mixed |
|
18 mutual and nested (co)recursion. Mixed (co)recursion enables type definitions |
|
19 involving both datatypes and codatatypes, such as the type of finitely branching |
|
20 trees of possibly infinite depth. The framework draws heavily from category |
|
21 theory. |
|
22 |
|
23 <p> |
|
24 The package is described in the following paper: |
|
25 |
|
26 <ul> |
|
27 <li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br> |
|
28 Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br> |
|
29 <i>Logic in Computer Science (LICS 2012)</i>, 2012. |
|
30 </ul> |
|
31 |
|
32 <p> |
|
33 The main entry point for applications is <tt>Codatatype.thy</tt>. |
|
34 The <tt>Examples</tt> directory contains various examples of (co)datatypes, |
|
35 including the examples from the paper. |
|
36 |
|
37 <p> |
|
38 The key notion underlying the package is that of a <i>bounded natural functor</i> |
|
39 (<i>BNF</i>)—an enriched type constructor satisfying specific properties |
|
40 preserved by interesting categorical operations (composition, least fixed point, |
|
41 and greatest fixed point). The <tt>Basic_BNFs.thy</tt> file registers |
|
42 various basic types, notably for sums, products, function spaces, finite sets, |
|
43 multisets, and countable sets. Custom BNFs can be registered as well. |
|
44 |
|
45 <p> |
|
46 <b>Warning:</b> The package is under development. Future versions are expected |
|
47 to support multiple constructors and selectors per (co)datatype (instead of a |
|
48 single <i>fld</i> or <i>unf</i> constant) and provide a nicer syntax for |
|
49 (co)datatype and (co)recursive function definitions. Please contact |
|
50 any of |
|
51 <a href="mailto:traytel@in.tum.de">the</a> |
|
52 <a href="mailto:popescua@in.tum.de">above</a> |
|
53 <a href="mailto:blanchette@in.tum.de">authors</a> |
|
54 if you have questions or comments. |
|
55 |
|
56 </body> |
|
57 |
|
58 </html> |