Type Checker Implementation

Hello,

I am trying to implement a type checker using OCaml. An example of the type checker rules is : 

γ ⊢ e:τ , γ ⊢ c:τ cmd
----------------------
γ ⊢ While e do c:τ cmd

1: τtypes are for the security levels, for example high or low levels.

2:a command that has the form τ cmdmeans command c has this type only if every assignment in c is to a variable whose security level is τ or higher.

So the rule means: in a 'While e do c' command, if e has a τ level security, then every assignment in c should be to a variable whose security level is τ or higher.  

Can you help me how can I implement this rule in OCaml?

Or an example of implementation of this type checker using OCaml?
(This type checker was introduced by Smith, G. and Volpano, D. in an article:  A Type-Based Approach to
Program  Security. 1997.)

Regards,
Arash
 
--
Arash Alavi
Department of Computer Engineering & Information Technology
Amirkabir University of Technology
Email(s): [email protected] , [email protected] page: http://ceit.aut.ac.ir/~arash.alavi