References to programming languages based on conditional logics Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\to B$ reads "$A$ causes "B", or probabilistic conditioning "$A|B$", which reads "$A$ given $B$"). 

Typically these logics are studied model-theoretically, but I've wondered about their applications to programming language design (for example, to type imperative actions). 

I'd appreciate references to their proof theory (ie, sequent calculus/natural deduction), or to programming languages with types based on these kinds of modal operators. 

Thanks!

EDIT: The Stanford Encyclopedia of Philosophy has a nice introduction to the subject.
Check these references:

Programming languages CondLP and CondLP+: 

Gabbay, Giordano,  Martelli, Olivetti, Sapino, Conditional reasoning in logic programming,  Journal of Logic Programming, Volume 44, Issues 1-3, 1 July 2000, Pages 37-74 

Claudia, Oliveira, The implementation of CondLP, Lecture Notes in Computer Science, 1996, Volume 1085/1996, 713-715

Gabbay, Giordano, Martelli, Olivetti, Conditional logic programming, Proc. 11th Int. Conf. on Logic Programming, Santa Margherita Ligure, pages 272–289, 1994.

References to proof theory:

Olivetti, Pozzato, Schwind, A sequent calculus and a theorem prover for standard conditional logics, Journal ACM Transactions on Computational Logic (TOCL), Volume 8 Issue 4, August 2007