diff --git a/icfp-2016/examples/db-types-fail.rkt b/icfp-2016/examples/db-types-fail.rkt
new file mode 100644
index 0000000..32b3ade
--- /dev/null
+++ b/icfp-2016/examples/db-types-fail.rkt
@@ -0,0 +1,8 @@
+#lang typed/racket/base
+
+;(define-new-subtype Database (database (Listof Table)))
+;;; Issue 1: need (Listof T *)
+;;(define-new-subtype Table (table (Pairof Symbol (Listof T))))
+;(define-new-subtype Table (table (Pairof Symbol (Listof Any))))
+;
+;(define-type Me (Database (Table 'word (List Natural String))))
diff --git a/icfp-2016/examples/map.rkt b/icfp-2016/examples/map.rkt
new file mode 100644
index 0000000..b026009
--- /dev/null
+++ b/icfp-2016/examples/map.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket/base
+(require trivial/no-colon)
+(define (cite (p : String) (d : String))
+    (printf "~a v. ~a, U.S.\n" p d))
+(define plaintiff*
+  '("Mistretta" "Rasul" "Chisholm"))
+(define defendant*
+  '("U.S." "Bush" "Georgia"))
+(void (map cite plaintiff* defendant*))
diff --git a/icfp-2016/examples/procedure-fail.rkt b/icfp-2016/examples/procedure-fail.rkt
new file mode 100644
index 0000000..54b1398
--- /dev/null
+++ b/icfp-2016/examples/procedure-fail.rkt
@@ -0,0 +1,18 @@
+#lang typed/racket/base
+
+;; Apply seems to work fine with arity checking.
+;; That's good because I'd rather the type system tracked arity
+;;  than me reflecting it from a `define`.
+
+;; -----------------------------------------------------------------------------
+
+;; Works great
+;(define (f x y)
+;  (+ x y))
+;
+;(apply f '(1 3 4))
+
+(define (cons3 x y z)
+  (cons x (cons y z)))
+
+(map cons3 '() '() '())
diff --git a/icfp-2016/examples/typed-racket-db.rkt b/icfp-2016/examples/typed-racket-db.rkt
new file mode 100644
index 0000000..7aaff33
--- /dev/null
+++ b/icfp-2016/examples/typed-racket-db.rkt
@@ -0,0 +1,25 @@
+#lang typed/racket/base
+
+;; Example using the db library in Typed Racket
+;; - require/typed gives specific type
+;; - rename-in allows multiple specific types in a file (just need to deal with renamings)
+
+;; -----------------------------------------------------------------------------
+
+(require/typed db
+  (#:opaque Connection connection?)
+  (postgresql-connect (->* () (#:user String #:database String) Connection)))
+
+(require/typed (prefix-in w: db)
+  (w:query-row (-> Connection String Any * (Vector Natural String))))
+
+(require/typed (prefix-in s: db)
+  (s:query-row (-> Connection String Any * (Vector Natural Natural))))
+
+;; -----------------------------------------------------------------------------
+
+(define c (postgresql-connect #:user "ben" #:database "ipoe"))
+(define r0 (w:query-row c "SELECT * FROM word WHERE word.word=$1" "blossoms"))
+(define r1 (s:query-row c "SELECT * FROM word_syllables WHERE word_syllables.word=$1" (vector-ref r0 0)))
+(displayln r0)
+(displayln r1)