diff --git a/book/book.toml b/book/book.toml
index 7d9bc99d..d6f4cfb1 100644
--- a/book/book.toml
+++ b/book/book.toml
@@ -4,3 +4,6 @@ language = "en"
multilingual = false
src = "src"
title = "The Aiken Programming Language"
+
+[output.html]
+mathjax-support = true
diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index ed30ec96..8800aba4 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -1,8 +1,8 @@
# Summary
-- [Intro](./introduction.md)
+- [Introduction](./introduction.md)
- [Untyped Plutus Core](./uplc.md)
-- [Guides](./guides.md)
- - [Transactions](./guides/transactions.md)
- - [Fee estimation without a node](./guides/transactions/fee_estimation.md)
+ - [Syntax](./uplc/syntax.md)
+ - [Command-line utilities](./uplc/cli.md)
+ - [Builtins](./uplc/builtins.md)
- [Resources](./resources.md)
diff --git a/book/src/guides.md b/book/src/guides.md
deleted file mode 100644
index abae4dea..00000000
--- a/book/src/guides.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Guides
-
-- [Transactions](./guides/transactions.md)
- - [Fee estimation without a node](./guides/transactions/fee_estimation.md)
diff --git a/book/src/guides/transactions.md b/book/src/guides/transactions.md
deleted file mode 100644
index f54d0601..00000000
--- a/book/src/guides/transactions.md
+++ /dev/null
@@ -1,3 +0,0 @@
-# Transactions
-
-- [Fee estimation without a node](./transactions/fee_estimation.md)
diff --git a/book/src/guides/transactions/fee_estimation.md b/book/src/guides/transactions/fee_estimation.md
deleted file mode 100644
index 04fa77d9..00000000
--- a/book/src/guides/transactions/fee_estimation.md
+++ /dev/null
@@ -1 +0,0 @@
-# Fee estimation without a node
diff --git a/book/src/introduction.md b/book/src/introduction.md
index aac49161..e6cdd836 100644
--- a/book/src/introduction.md
+++ b/book/src/introduction.md
@@ -1,4 +1,4 @@
-# Intro
+# Introduction
Aiken is a new programming language and toolchain for developing
smart contracts on the [Cardano](https://cardano.org) blockchain.
@@ -43,6 +43,4 @@ The Aiken project is made up of a few different components. The two most importa
ones are the high level Aiken language for writing smart contracts and a rust library
for working with Untyped Plutus Core.
-### The Language
-
-### Untyped Plutus Core
+Learn more about them in the next sections of this book.
diff --git a/book/src/uplc.md b/book/src/uplc.md
index a66f129c..11a0cf30 100644
--- a/book/src/uplc.md
+++ b/book/src/uplc.md
@@ -1,35 +1,23 @@
# Untyped Plutus Core
-## Usage
+One key feature of Aiken is how it helps you manipulate Untyped Plutus Core
+(abbrev. UPLC in short). UPLC is ultimately the format whereby codes gets
+executed on-chain. This is pretty-much as low-level as you can get when it
+comes to Cardano smart-contracts.
-For now the command line application can only encode/decode Untyped Plutus Core
-to/from it's on chain format. See the roadmap below for a list of planned features and goals.
+Understanding how UPLC works, and having the right tools to troubleshoot
+UPLC programs can be handy when developing contracts on Cardano. Fortunately,
+this is something Aiken can help you with.
-```sh
-# help
-aiken help
-
-# compile an untyped plutus core program to flat
-aiken uplc flat program.uplc
-
-aiken uplc flat program.uplc --print
-
-# output
-00001011 00010110 00100001 01001000
-00000101 10000001
-
-aiken uplc flat program.uplc --out=something.flat
-
-# decode an untyped plutus core program from flat
-aiken uplc unflat program.flat
-
-aiken uplc unflat program.flat --print
-
-# output
-(program
- 11.22.33
- (con integer 11)
-)
-
-aiken uplc unflat program.flat --out=something.uplc
-```
+> **Note**
+>
+> While UPLC has erased any _explicit_ notion of types; functions, variables and
+> constants are still _implicitly_ typed and, an interpreter will raise errors
+> when encountering a type mismatch.
+>
+> For the sake of simplicity, we might speak about the type-signature of
+> builtin functions such as `addInteger` which, in principle, only has a
+> concrete meaning in Typed Plutus Core. Hence, even though they are _untyped_,
+> we often think of UPLC programs has having implicit types, as if they were
+> originally _typed_ programs whose types had simply been erased (in fact,
+> that's exactly what they are).
diff --git a/book/src/uplc/builtins.md b/book/src/uplc/builtins.md
new file mode 100644
index 00000000..956c10fd
--- /dev/null
+++ b/book/src/uplc/builtins.md
@@ -0,0 +1,80 @@
+# Builtins
+
+| Builtins | Type Args | Term Args | Result |
+| --- | --- | --- | --- |
+| `ifThenElse`[^1] | \\(α\\) | (bool, \\(α\\), \\(α\\)) | \\(α\\) |
+| --- | --- | --- | --- |
+| `addInteger` | \- | (integer, integer) | integer |
+| `subtractInteger` | \- | (integer, integer) | integer |
+| `multiplyInteger` | \- | (integer, integer) | integer |
+| `divideInteger` | \- | (integer, integer) | integer |
+| `modInteger` | \- | (integer, integer) | integer |
+| `quotientInteger` | \- | (integer, integer) | integer |
+| `remainderInteger` | \- | (integer, integer) | integer |
+| `equalsInteger` | \- | (integer, integer) | bool |
+| `lessThanInteger` | \- | (integer, integer) | bool |
+| `lessThanEqualsInteger` | \- | (integer, integer) | bool |
+| `greaterThanInteger` | \- | (integer, integer) | bool |
+| `greaterThanEqualsInteger` | \- | (integer, integer) | bool |
+| --- | --- | --- | --- |
+| `appendString` | \- | (string, string) | string |
+| `emptyString` | \- | (string) | bool |
+| `equalsString` | \- | (string, string) | bool |
+| `encodeUtf8` | \- | (string) | bytestring |
+| --- | --- | --- | --- |
+| `appendByteString` | \- | (bytestring, bytestring) | bytestring |
+| `consByteString` | \- | (integer, bytestring) | bytestring |
+| `indexByteString` | \- | (integer, bytestring) | integer |
+| `sliceByteString` | \- | (integer, integer, bytestring) | bytestring |
+| `lengthOfByteString` | \- | (bytestring) | integer |
+| `emptyByteString` | \- | (bytestring) | bool |
+| `equalsByteString` | \- | (bytestring, bytestring) | bool |
+| `lessThanByteString` | \- | (bytestring, bytestring) | bool |
+| `lessThanEqualsByteString` | \- | (bytestring, bytestring) | bool |
+| `greaterThanByteString` | \- | (bytestring, bytestring) | bool |
+| `greaterThanEqualsByteString` | \- | (bytestring, bytestring) | bool |
+| `decodeUtf8` | \- | (bytestring) | string |
+| --- | --- | --- | --- |
+| `chooseData`[^2] | \\(α\\) | (data, \\(α\\), \\(α\\), \\(α\\), \\(α\\), \\(α\\)) | \\(α\\) |
+| `constrData` | \- | (integer, list data) | data |
+| `unConstrData` | \- | data | (integer, list data) |
+| `iData` | \- | (integer) | data |
+| `unIData` | \- | (data) | integer |
+| `bData` | \- | (bytestring) | data |
+| `unBData` | \- | (data) | bytestring |
+| `mapData` | \- | (list (pair data data)) | data |
+| `unMapData` | \- | (data) | list (pair data data) |
+| `listData` | \- | (list data) | data |
+| `unListData` | \- | (data) | list data |
+| `equalsData` | \- | (data, data) | bool |
+| `serialiseData` | \- | (data) | bytestring |
+| --- | --- | --- | --- |
+| `chooseList`[^3] | \\(α, β\\) | (list \\(α\\), \\(β\\), \\(β\\)) | \\(β\\) |
+| `mkNilData` | \\(α\\) | (unit) | list \\(α\\) |
+| `mkCons` | \\(α\\) | (\\(α\\), list \\(α\\)) | list \\(α\\) |
+| `headList` | \\(α\\) | (list \\(α\\)) | \\(α\\) |
+| `tailList` | \\(α\\) | (list \\(α\\)) | list \\(α\\) |
+| `nullList` | \\(α\\) | (list \\(α\\)) | bool |
+| --- | --- | --- | --- |
+| `mkPairData` | \\(α, β\\) | (\\(α\\), \\(β\\)) | pair \\(α\\) \\(β\\) |
+| `fstPair` | \\(α, β\\) | pair \\(α\\) \\(β\\) | \\(α\\) |
+| `sndPair` | \\(α, β\\) | pair \\(α\\) \\(β\\) | \\(β\\) |
+| --- | --- | --- | --- |
+| `sha2_256` | \- | (bytestring) | bytestring |
+| `sha3_256` | \- | (bytestring) | bytestring |
+| `blake2b_256` | \- | (bytestring) | bytestring |
+| --- | --- | --- | --- |
+| `verifyEd25519Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
+| `verifyEcdsaSecp256k1Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
+| `verifySchnorrSecp256k1Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
+| --- | --- | --- | --- |
+| `error` | \\(α\\) | (unit) | \\(α\\) |
+| `trace` | \\(α\\) | (string, \\(α\\)) | \\(α\\) |
+
+[^1]: Returns the second argument when the predicate is `True`, and the third argument when `False`.
+
+[^2]: Each argument corresponds to each of the constructors of a builtin data (in this order): constr, map, list, integer and bytestring. The evaluation will continue with whatever branch actually corresponds to the given term value.
+
+[^3]: Returns the second argument when the list is empty, and the third argument otherwise.
+
+[^4]: Arguments are respectively: the public key, the message and the signature
diff --git a/book/src/uplc/cli.md b/book/src/uplc/cli.md
new file mode 100644
index 00000000..1d9e2d1e
--- /dev/null
+++ b/book/src/uplc/cli.md
@@ -0,0 +1,128 @@
+# Command-line utilities
+
+## Evaluation
+
+Let's consider the following basic program:
+
+program_1.uplc
+
+```
+(program
+ 2.0.0
+ [ [ (builtin addInteger) (con integer 16) ] (con integer 26) ]
+)
+```
+
+We can evaluate this program using Aiken's cli via:
+
+```console
+$ aiken uplc eval program_1.uplc
+```
+
+```
+Result
+------
+(con integer 42)
+
+Costs
+-----
+cpu: 321577
+memory: 602
+
+Budget
+------
+cpu: 9999678423
+memory: 13999398
+```
+
+The output indicates the result of the evaluation (`42`) as well as the
+execution cost of that program, both in terms of CPU and memory usage.
+
+Note that the command also accepts arguments. So, for example, if we modify our
+program into a function that accepts an argument as follows:
+
+program_2.uplc
+
+```
+(program
+ 2.0.0
+ (lam x [ [ (builtin addInteger) (con integer 16) ] x ])
+)
+```
+
+You can then instrument Aiken to provide arguments upon calling the program by
+simply appending them to the `eval` command:
+
+```console
+$ aiken uplc eval program_2.uplc "(con integer 26)"
+```
+
+```
+Result
+------
+(con integer 42)
+```
+
+## Formatting
+
+Because writing UPLC by hand can be a tedious task, Aiken provides a quick way to automatically format
+a UPLC program via the `fmt` command. By default, the command override the file given as input, but you
+can also simply prints the result to stdout using `--print`. For example:
+
+```console
+$ aiken uplc fmt program_2.uplc --print
+```
+
+```
+(program
+ 2.0.0
+ (lam x [ [ (builtin addInteger) (con integer 16) ] x ])
+)
+```
+
+## Converting to/from bytecode
+
+So far, we've been representing UPLC programs using a high-level syntax. In
+practice, however, UPLC programs are compiled into bytecode when submitted
+on-chain.
+
+Aiken provides means to convert a high-level UPLC program into a low-level flat
+bytecode − and vice-versa, via the `flat` and `unflat` commands. For example:
+
+```console
+$ aiken uplc flat program_1.uplc --print
+```
+
+```
+00000010 00000000 00000000 00110011
+01110000 00001001 00000001 00000010
+01000000 01101001
+```
+
+The `--print` flag instruments the command-line to print everything on stdout
+in a readable way. Without the flag, the command creates a file `program_1.flat`
+next to `program_1.uplc`.
+
+> **Note**
+>
+> `aiken uplc flat program.uplc`
+>
+> and
+>
+> `aiken uplc flat program.uplc --out program.flat`
+>
+> are therefore equivalent.
+
+From there, one can recover a UPLC high-level syntax from a flat program using
+`unflat` as such:
+
+```console
+$ aiken uplc unflat program_1.flat --print
+```
+
+```
+(program
+ 2.0.0
+ [ [ (builtin addInteger) (con integer 16) ] (con integer 26) ]
+)
+```
diff --git a/book/src/uplc/syntax.md b/book/src/uplc/syntax.md
new file mode 100644
index 00000000..a14f6b51
--- /dev/null
+++ b/book/src/uplc/syntax.md
@@ -0,0 +1,74 @@
+# Syntax
+
+Let's start with a little reminder about the syntax. The complete syntax for Untyped Plutus Core comes from the original [Formal Specification of the Plutus Core Language](https://hydra.iohk.io/build/14133599/download/1/plutus-core-specification.pdf).
+
+## Primitive Types
+
+Plutus Core has 5 primitive types: `unit`, `bool`, `integer`, `string` and
+`bytestring`. One can construct constants using the `con` keyword, followed by
+the name of the primitive type and its value.
+
+- Unit is denoted `()`;
+- Bool are `True` or `False`;
+- Bytestrings are denoted with a leading `#` followed by an hexadecimal sequence;
+- Strings are UTF-8 text strings, between double quotes `"`.
+
+| Primitive Type | Example |
+| --- | --- |
+| `unit` | `con unit ()` |
+| `bool` | `con bool True` |
+| `integer` | `con integer 42` |
+| `bytestring` | `con bytestring #41696b656e` |
+| `string` | `con string "Aiken"` |
+
+## Functions
+
+A function (or simply, lambda) is constructed with the keyword `lam` followed
+by a variable name, and a term (i.e. a constant, another function, etc..). One
+can apply variables to a function using squared brackets `[ ]`.
+
+For example: `[ (lam x x) (con integer 42) ]`.
+
+This little excerpt constructs a function that takes an argument `x` and returns
+it; to which we immediately apply the constant `42`. If we were to evaluate this
+program, it would simply output: `42`.
+
+## Builtins
+
+Plutus Core comes with a set of builtins functions which comes in handy to
+define certain operations. Incidentally, there's no _operator_ even for basic
+arithmetic operations, everything comes as a builtin.
+
+You'll notice also that some builtins are very domain specific and tailored to
+operations you'd expect a smart-contract to perform on a blockchain. Hence, new
+builtins may be added in the future to address specific use cases that emerge.
+
+Builtins are called with the keyword `builtin` followed by their names. They may
+take one, two, three or really any number of arguments. The complete list of builtins
+is given [in annexe](./uplc/builtins.md).
+
+## Delay & Force
+
+Plutus Core has the notion of type abstractions and type instantiations. That is, like lambdas are functions over term values, abstractions are functions over types. These abstractions allow to represent polymorphic types (such as, a list of elements, or an option type). UPLC has gotten rid of the types, but introduces two new keywords in order to preserve the abstractions in some form.
+
+- `force` can be used on a polymorphic function to instantiate one type-parameter. For example, the branches of a builtin `ifThenElse` can be of any type -- though they have to be the same for both branches. In fact, `ifThenElse` has one type parameter. To be called, it must therefore be forced once: `[ [ [ force (builtin ifThenElse) p ] x ] y ]`
+
+- Similarly, `delay` can be used to defer the evaluation of a certain term; this allows to artificially construct or preserve type abstractions, but also, to introduce a certain level of laziness in parts of the program.
+
+## Data
+
+In addition to primitive types, Plutus Core also has a more generalized `data`
+data-type which is meant to represent any possible data-type in a program.
+
+> **TODO**: Give additional detail about how the serialization is done and how
+> to construct a Data.
+>
+> In particular, revisit after [#34](https://github.com/txpipe/aiken/issues/34)
+> since the introduction of "list" and "pair" keywords may come in handy.
+
+## Programs
+
+Finally, UPLC programs are wraps in a `program` declaration, which indicates
+the version (e.g. `1.0.0`) of Plutus Core that this programs uses. You don't
+have to worry about that too much. Aiken supports the latest Plutus version
+(`2.0.0`).