src/HOL/BNF/README.html
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 52794 aae782070611
child 54540 5d7006e9205e
permissions -rw-r--r--
renamed theory file
blanchet@48975
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
blanchet@48975
     2
blanchet@48975
     3
<html>
blanchet@48975
     4
blanchet@48975
     5
<head>
blanchet@48975
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
blanchet@49509
     7
  <title>BNF Package</title>
blanchet@48975
     8
</head>
blanchet@48975
     9
blanchet@48975
    10
<body>
blanchet@48975
    11
blanchet@49509
    12
<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
blanchet@48975
    13
(BNFs)</h3>
blanchet@48975
    14
blanchet@48975
    15
<p>
blanchet@49509
    16
The <i>BNF</i> package provides a fully modular framework for constructing
blanchet@49509
    17
inductive and coinductive datatypes in HOL, with support for mixed mutual and
blanchet@49509
    18
nested (co)recursion. Mixed (co)recursion enables type definitions involving
blanchet@49509
    19
both datatypes and codatatypes, such as the type of finitely branching trees of
blanchet@49509
    20
possibly infinite depth. The framework draws heavily from category theory.
blanchet@48975
    21
blanchet@48975
    22
<p>
blanchet@48975
    23
The package is described in the following paper:
blanchet@48975
    24
blanchet@48975
    25
<ul>
blanchet@52794
    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>
blanchet@48975
    27
  Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
blanchet@48975
    28
  <i>Logic in Computer Science (LICS 2012)</i>, 2012.
blanchet@48975
    29
</ul>
blanchet@48975
    30
blanchet@48975
    31
<p>
blanchet@49509
    32
The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt>
blanchet@49509
    33
directory contains various examples of (co)datatypes, including the examples
blanchet@49509
    34
from the paper.
blanchet@48975
    35
blanchet@48975
    36
<p>
blanchet@48975
    37
The key notion underlying the package is that of a <i>bounded natural functor</i>
blanchet@48975
    38
(<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
blanchet@48975
    39
preserved by interesting categorical operations (composition, least fixed point,
blanchet@49509
    40
and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
blanchet@49509
    41
files register various basic types, notably for sums, products, function spaces,
blanchet@49509
    42
finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
blanchet@48975
    43
blanchet@48975
    44
<p>
blanchet@49509
    45
<b>Warning:</b> The package is under development. Please contact any nonempty
blanchet@49509
    46
subset of
blanchet@48975
    47
<a href="mailto:traytel@in.tum.de">the</a>
blanchet@48975
    48
<a href="mailto:popescua@in.tum.de">above</a>
blanchet@48975
    49
<a href="mailto:blanchette@in.tum.de">authors</a>
blanchet@48975
    50
if you have questions or comments.
blanchet@48975
    51
blanchet@48975
    52
</body>
blanchet@48975
    53
blanchet@48975
    54
</html>