diff --git a/bn.rkt b/bn.rkt
deleted file mode 100644
index dd2184f..0000000
--- a/bn.rkt
+++ /dev/null
@@ -1,115 +0,0 @@
-#lang racket
-
-;;; dds/bn
-
-;;; This module provides some quick definitions for running Boolean
-;;; networks.  A Boolean network is a set of Boolean variables which
-;;; are updated according to their corresponding update functions.
-;;; The variables to be updated at each step are given by the mode.
-
-(require "utils.rkt")
-
-(provide
- ;; Functions
- update make-state make-bn-funcs update-func-form->update-func
- bn-form->bn make-bn-forms
- ;; Syntax
- st bn)
-
-
-;;; =================
-;;; Basic definitions
-;;; =================
-
-(define-type Variable Symbol)
-
-;;; A state of a Boolean network is a mapping from the variables of the
-;;; network to their Boolean values.
-(define-type State (HashTable Variable Boolean))
-
-;;; An update function is a Boolean function computing a Boolean value
-;;; from the given state.
-(define-type UpdateFunc (-> State Boolean))
-
-;;; A Boolean network is a mapping from its variables to its update
-;;; functions.
-(define-type Network (HashTable Variable UpdateFunc))
-
-;;; Given a state s updates all the variables from xs.  This
-;;; corresponds to a parallel mode.
-(: update (-> Network State (Listof Variable) State))
-(define (update bn  ; the Boolean network
-                s   ; the state to operate on
-                xs) ; the variables to update
-  (let ([new-s : State (hash-copy s)])
-    (for ([x xs])
-      (let ([f (hash-ref bn x)])
-        (hash-set! new-s x (f s))))
-    new-s))
-
-;;; A version of make-hash restricted to creating Boolean states.
-(: make-state (-> (Listof (Pairof Variable Boolean)) State))
-(define (make-state mappings)
-  (make-hash mappings))
-
-;;; A shortcut for make-state.
-(define-syntax-rule (st mappings) (make-state mappings))
-
-;;; A version of make-hash restricted to creating Boolean networks.
-(: make-bn-funcs (-> (Listof (Pairof Variable UpdateFunc)) Network))
-(define (make-bn-funcs funcs)
-  (make-hash funcs))
-
-
-;;; =========================================
-;;; Syntactic description of Boolean networks
-;;; =========================================
-
-;;; An UpdateFuncForm is any form which can appear as a body of a
-;;; Boolean function and which can be evaluated with eval.  For
-;;; example, '(and x y (not z)).
-(define-type UpdateFuncForm Any)
-
-;;; A Boolean network form is a mapping from its variables to the
-;;; forms of their update functions.
-(define-type NetworkForm (HashTable Variable UpdateFuncForm))
-
-;;; Build an update function from an update function form.
-#;(: update-func-form->update-func (-> UpdateFuncForm UpdateFunc))
-(define (update-func-form->update-func form)
-  (lambda ([s : State])
-    (cast (eval-with1 (cast s (HashTable Variable Any)) form) Boolean)))
-
-;;; Build a Network from a Network form.
-(: bn-form->bn (-> NetworkForm Network))
-(define (bn-form->bn bnf)
-  (make-hash
-   (hash-map bnf (lambda ([x : Variable] [form : UpdateFuncForm])
-                   (cons x (update-func-form->update-func form))))))
-
-;;; Build a network from a list of pairs of forms of update functions.
-(: make-bn-forms (-> (Listof (Pairof Variable UpdateFuncForm)) Network))
-(define (make-bn-forms forms)
-  (bn-form->bn (make-hash forms)))
-
-;;; A shortcut for make-bn-forms.
-(define-syntax-rule (bn forms) (make-bn-forms forms))
-
-
-;;; ============================
-;;; Inferring interaction graphs
-;;; ============================
-
-;;; I allow any syntactic forms in definitions of Boolean functions.
-;;; I can still find out which Boolean variables appear in those
-;;; syntactic form, but I have no reliable syntactic means of finding
-;;; out what kind of action do they have (inhibition or activation)
-;;; since I cannot do Boolean minimisation (e.g., I cannot rely on not
-;;; appearing before a variable, since (not (not a)) is equivalent
-;;; to a).  On the other hand, going through all Boolean states is
-;;; quite resource-consuming and thus not always useful.
-;;;
-;;; In this section I provide inference of both unsigned and signed
-;;; interaction graphs, but since the inference of signed interaction
-;;; graphs is based on analysing the dynamics of the networks, it may
-;;; be quite resource-consuming.
diff --git a/bn-tests.rkt b/networks-tests.rkt
similarity index 72%
rename from bn-tests.rkt
rename to networks-tests.rkt
index e03c456..04a0b8e 100644
--- a/bn-tests.rkt
+++ b/networks-tests.rkt
@@ -1,21 +1,21 @@
-#lang typed/racket
+#lang racket
 
-;;; Tests for dds/bn.
+;;; Tests for dds/networks.
 
-(require typed/rackunit "bn.rkt")
+(require rackunit "networks.rkt")
 
 ;;; This test case sets up the following Boolean network:
 ;;; x1 = x1 AND NOT x2
 ;;; x2 = NOT x2
 (test-case "Basic definitions"
-  (let* ([f1 (λ ([s : State])
+  (let* ([f1 (λ (s)
                (let ([x1 (hash-ref s 'x1)]
                      [x2 (hash-ref s 'x2)])
                  (and x1 (not x2))))]
-         [f2 (λ ([s : State])
+         [f2 (λ (s)
                (let ([x2 (hash-ref s 'x2)])
                  (not x2)))]
-         [bn (make-bn-funcs `((x1 . ,f1) (x2 . ,f2)))])
+         [bn (make-network-from-functions `((x1 . ,f1) (x2 . ,f2)))])
 
     (test-case "One-step syncronous update"
       (let* ([s (make-state '((x1 . #t) (x2 . #f)))]
@@ -33,12 +33,12 @@
 
 (test-case "Syntactic description of Boolean networks"
   (let ([s (make-state '((x . #t) (y . #f)))]
-        [f (update-func-form->update-func '(and x y))])
+        [f (update-function-form->update-function '(and x y))])
     (check-equal? (f s) #f))
-  (let ([bn1 (bn-form->bn (make-hash '((a . (and a b)) (b . (not b)))))]
-        [bn2 (make-bn-forms '((a . (and a b))
-                              (b . (not b))))]
-        [bn3 (bn '((a . (and a b))
+  (let ([bn1 (network-form->network (make-hash '((a . (and a b)) (b . (not b)))))]
+        [bn2 (make-network-from-forms '((a . (and a b))
+                                        (b . (not b))))]
+        [bn3 (nn '((a . (and a b))
                    (b . (not b))))]
         [s (st '((a . #t) (b . #t)))])
     (check-equal? ((hash-ref bn1 'a) s) #t)
diff --git a/networks.rkt b/networks.rkt
new file mode 100644
index 0000000..eedc28c
--- /dev/null
+++ b/networks.rkt
@@ -0,0 +1,120 @@
+#lang racket
+
+;;; dds/networks
+
+;;; This module provides some quick definitions for and analysing
+;;; network models.  A network is a set of variables which are updated
+;;; according to their corresponding update functions.  The variables
+;;; to be updated at each step are given by the mode.
+;;;
+;;; This model can generalise Boolean networks, TBANs, multivalued
+;;; networks, etc.
+
+(require "utils.rkt")
+
+(provide
+ ;; Functions with contracts
+ (contract-out [update (-> network? state? (listof variable?) state?)]
+               [make-state (-> (listof (cons/c symbol? any/c)) state?)]
+               [make-network-from-functions (-> (listof (cons/c symbol? update-function?)) network?)]
+               [update-function-form->update-function (-> update-function-form? update-function?)]
+               [network-form->network (-> network-form? network?)]
+               [make-network-from-forms (-> (listof (cons/c symbol? update-function-form?))
+                                            network?)])
+ ;; Functions
+ variable? state? update-function? update-function-form? network-form?
+ ;; Contracts
+ state/c network/c
+ ;; Syntax
+ st nn)
+
+
+;;; =================
+;;; Basic definitions
+;;; =================
+
+(define variable? symbol?)
+
+;;; A state of a network is a mapping from the variables of the
+;;; network to their values.
+(define state? variable-mapping?)
+(define state/c (flat-named-contract 'state state?))
+
+;;; An update function is a function computing a value from the given
+;;; state.
+(define update-function? (-> state? any/c))
+
+;;; A network is a mapping from its variables to its update functions.
+(define network? variable-mapping?)
+(define network/c (flat-named-contract 'network network?))
+
+;;; Given a state s updates all the variables from xs.  This
+;;; corresponds to a parallel mode.
+(define (update bn  ; the Boolean network
+                s   ; the state to operate on
+                xs) ; the variables to update
+  (let ([new-s (hash-copy s)])
+    (for ([x xs])
+      (let ([f (hash-ref bn x)])
+        (hash-set! new-s x (f s))))
+    new-s))
+
+;;; A version of make-hash restricted to creating network states (see
+;;; contract).
+(define (make-state mappings) (make-hash mappings))
+
+;;; A shortcut for make-state.
+(define-syntax-rule (st mappings) (make-state mappings))
+
+;;; A version of make-hash restricted to creating networks.
+(define (make-network-from-functions funcs) (make-hash funcs))
+
+
+;;; =================================
+;;; Syntactic description of networks
+;;; =================================
+
+;;; An update function form is any form which can appear as a body of
+;;; a function and which can be evaluated with eval.  For example,
+;;; '(and x y (not z)) or '(+ 1 a (- b 10)).
+(define update-function-form? any/c)
+
+;;; A Boolean network form is a mapping from its variables to the
+;;; forms of their update functions.
+(define network-form? variable-mapping?)
+
+;;; Build an update function from an update function form.
+(define (update-function-form->update-function form)
+  (lambda (s) (eval-with s form)))
+
+;;; Build a network from a network form.
+(define (network-form->network bnf)
+  (make-hash
+   (hash-map bnf (lambda (x form)
+                   (cons x (update-function-form->update-function form))))))
+
+;;; Build a network from a list of pairs of forms of update functions.
+(define (make-network-from-forms forms)
+  (network-form->network (make-hash forms)))
+
+;;; A shortcut for make-network-from-forms.
+(define-syntax-rule (nn forms) (make-network-from-forms forms))
+
+
+;;; ============================
+;;; Inferring interaction graphs
+;;; ============================
+
+;;; I allow any syntactic forms in definitions of Boolean functions.
+;;; I can still find out which Boolean variables appear in those
+;;; syntactic form, but I have no reliable syntactic means of finding
+;;; out what kind of action do they have (inhibition or activation)
+;;; since I cannot do Boolean minimisation (e.g., I cannot rely on not
+;;; appearing before a variable, since (not (not a)) is equivalent
+;;; to a).  On the other hand, going through all Boolean states is
+;;; quite resource-consuming and thus not always useful.
+;;;
+;;; In this section I provide inference of both unsigned and signed
+;;; interaction graphs, but since the inference of signed interaction
+;;; graphs is based on analysing the dynamics of the networks, it may
+;;; be quite resource-consuming.