The Coq mailing list

[Seokhyun Han <seokhyun AT cs.rhul.ac.uk>]

---------- Forwarded message ----------
Date: Thu, 7 Jun 2007 17:00:41 +0100 (BST)
From: Seokhyun Han 
<seokhyun AT cs.rhul.ac.uk>
To:  
<coq-club-request AT pauillac.inria.fr>
Subject: coq & Finance engineering


Dear all coq users,

I am Phd student of computer science in Royal Holloway, London university, 
and researching Dependent type theory and coercive subtyping. 

Personally, I am very interested in how to apply Coq to Finance 
engineering. I am writing this email to share this idea with other 
researchers using Coq. I hope to find someone interested in this idea.

For example, 

1. Can we define inductive data types for risky asset models(stock, 
bond, ...), which includes random processes by COQ ?

2. Can we prove a few important properties derived in Derivative markets 
and extract exact pricing algorithms by using COQ ?  

3. Is it possible to connect  COQ and Matlab ?  

and so on. 

If anybody is interested in above ideas, please email me. 

THanks.

seokhyun Han

email : 
seokhyun AT cs.rhul.ac.uk