unified expressions

I unified Boolean and real expressions into a single type. This cuts
down a lot of duplication in definitions and proofs. Moreover, we now
have if expressions. However, variable binding becomes more difficult
since an expression may have free variables of different types.
slightly stricter variant of syntactic horizon
generalise syntactic horizon
specialise type indexing
simplify type indexing of expression language
start formalising specialisation
change semantic representation of cash-flows

The semantic representation of cash-flows is "anti-symmetric" in the
sense that at any time t for which C[|c|]rho (t) is defined, the
semantics must satisfy that

C[|c|]rho (t) (p1,p2,c) = C[|c|]rho (t) (p2,p1,c)
proof of antisymmetry of the denotational semantics
start on extrinsic formalisation

This branch explores an extrinsic approach to formalising the contract
language. That is, instead of representing contract language's type
system using Coq's type system, we use explicit typing judgements. Our
hypothesis is that this extrinsic approach makes code extraction
simpler/possible.
equivalence and monotonicity
horizon
reduction semantics
extraction of horizon & reduction semantics
Merge branch 'master' into extrinsic

Conflicts:
	Coq/Denotational.v
	Coq/Extraction/Header.hs
	Coq/Horizon.v
	Coq/Syntax.v
Merge branch 'master' into extrinsic

Conflicts:
	Coq/Extraction/ContractExtracted.hs
Haskell combinators for constructing contracts

The combinators use HOAS, which is translated into de Bruijn-style
binders using the technique described in "Unembedding Domain-Specific
Languages".
remove Syntax.hs
complete Fractional instance for RExp
specialisation
Merge branch 'master' into extrinsic

Conflicts:
	Coq/Extraction/MonadExamples.hs