src/HOL/BNF/README.html
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 52794 aae782070611
child 54540 5d7006e9205e
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     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>BNF Package</title>
     8 </head>
     9 
    10 <body>
    11 
    12 <h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
    13 (BNFs)</h3>
    14 
    15 <p>
    16 The <i>BNF</i> package provides a fully modular framework for constructing
    17 inductive and coinductive datatypes in HOL, with support for mixed mutual and
    18 nested (co)recursion. Mixed (co)recursion enables type definitions involving
    19 both datatypes and codatatypes, such as the type of finitely branching trees of
    20 possibly infinite depth. The framework draws heavily from category theory.
    21 
    22 <p>
    23 The package is described in the following paper:
    24 
    25 <ul>
    26   <li><a href="http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic&mdash;Category Theory Applied to Theorem Proving</a>, <br>
    27   Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
    28   <i>Logic in Computer Science (LICS 2012)</i>, 2012.
    29 </ul>
    30 
    31 <p>
    32 The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt>
    33 directory contains various examples of (co)datatypes, including the examples
    34 from the paper.
    35 
    36 <p>
    37 The key notion underlying the package is that of a <i>bounded natural functor</i>
    38 (<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
    39 preserved by interesting categorical operations (composition, least fixed point,
    40 and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
    41 files register various basic types, notably for sums, products, function spaces,
    42 finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
    43 
    44 <p>
    45 <b>Warning:</b> The package is under development. Please contact any nonempty
    46 subset of
    47 <a href="mailto:traytel@in.tum.de">the</a>
    48 <a href="mailto:popescua@in.tum.de">above</a>
    49 <a href="mailto:blanchette@in.tum.de">authors</a>
    50 if you have questions or comments.
    51 
    52 </body>
    53 
    54 </html>