I've been wondering if there's a connection between good logics and good programming languages. It seems that logics are shown to be locally sound and complete whereas programming languages are shown to be type safe (preservation and progress).If there's a relationship could you please explain it and give some references so that I can follow up on it.
Is there a relationship between sound and complete in logic and type safety in PLs?
programming languages;logic;type theory
The concepts of local soundness and local completeness (which is Frank Pfenning's terminology, originally introduced in his paper with Rowan Davies, A Judgmental Reconstruction of Modal Logic) are a bit more specific than the standard concepts of soundness and completeness relative to a model as suggested in the title of your question (and as in Andrej's answer).  Under the Curry-Howard correspondence, local soundness and local completeness correspond exactly to $\beta$-reduction and $\eta$-expansion of typed terms, respectively.These are not quite preservation and progress, but preservation is closely related to (and usually relies on the fact that) $\beta$-reduction is type-preserving. The type safety theorem that results from combining preservation + progress is somewhat related to global soundness (in the sense of these lecture notes), which is just another name for the normalization/cut-elimination theorem for (a proof system for) a logic. Type safety is a weaker statement, though, since combining preservation with progress only guarantees that a term $t:A$ will either eventually reduce to a value $t \leadsto^* v$ such that $v:A$ or else fail to terminate. In contrast, the normalization theorem for a logic says that any proof $\pi$ of $A$ can definitely be reduced to a normal proof of $A$.PL designers have typically paid less attention to $\eta$-expansion, although this is starting to change in languages with more sophisticated type systems (such as proof assistants). In such languages, $\eta$-expansion (and hence local completeness) is closely related to the definitions of equality and/or subtyping.There is a bit more discussion of local soundness and completeness and their Curry-Howard interpretation in Pfenning's Logical Frameworks — A Brief Introduction.