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. 
References to programming languages based on conditional logics
reference request;lo.logic;pl.programming languages;type theory;proof theory
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-715Gabbay, Giordano, Martelli, Olivetti, Conditional logic programming, Proc. 11th Int. Conf. on Logic Programming, Santa Margherita Ligure, pages 272289, 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 