Logic vs. type system What's the difference between logic (in a narrow sense, i.e. a logical system such as ZOL, FOL, etc.) and type system?
I will sketch my understanding of this -- please correct if I err. Under propositions-as-types, they coincide. In propositions-as-some-types, a logic(al system) is a proper subset of the type system. In logic-enriched type theory (LTT), they are distinct components. "Untyped" always means "single-typed" (as in untyped $λ$-calculus, which has only functions), and describes the object level of the formalism (i.e. its objects belong to a single type); together with its meta level there are more types (e.g. the syntactic operators $λ$, . in $λ$-calculus). I'll finish with some examples of the possible combinations:
typed logic : FOL
typed nonlogic : a data type system
untyped logic : untyped lambda-calculus*
untyped nonlogic : a teapot
* not a logic but can encode one
 A: A set-theoretic foundational system is usually based on two main pillars:


*

*The deductive system of the theory, usually first-order classical logic;

*The body of axioms of the theory, such as $\mathsf{ZFC}$.


The type-theoretic approach is different from that of set-theory. Instead of sets, we place functions as the first class mathematical objects. Also, types get their meaning from the way we use them, having their corresponding formation, construction, elimination, computation (and possibly uniqueness) rules for each type.
The propositions-as-types correspondence states that it is possible to interpret logic within a type theory, by viewing the statement that we want to prove, typically a judgment of the form "proposition $A$ is true",
$$A \; \mathsf{true},$$
as the claim that the type that this proposition corresponds is inhabited,
$$\frac{a : A}{\mathsf{true}}.$$
There are interesting philosophical aspects to this interpretation (see e.g. Martin-Löf (1996)). But my main point here is that a type-theoretic foundation comprises both components of the set-theoretic approach mentioned above, as we can regard types as sets and propositions. 
Some examples are shown on the following table (for more see the Homotopy Type Theory Book):
$$\begin{array} {|c|}
\hline
\textsf{Types} & \textsf{Logic} & \textsf{Sets} \\ \hline
A & \text{proposition} & \text{set} \\ \hline
a:A & a\text{ is a proof of }A & a\text{ is an element of }A \\ \hline
A\rightarrow B & A \text{ implies } B & \text{set of functions from }A \text{ to }B\ \\ \hline
A\times B & A \text{ and } B & \text{cartesian product of }A \text{ and }B\ \\ \hline
\end{array}$$
A: In my understanding formal logic-systems (like FOL, propositional logic, etc) and type theories (or type systems) are all families of derivation systems: i.e. systems having an underlying set of formulas (usually described by a formal grammar) and inference rules defined on these formulas (which can be thought as operation for generating tree of formulas, the proofs).
These kind of formal systems differ in their presentations (the grammar for their languages and, consequently, their inference rules) but they are isomorphic (as derivation systems) as Curry-Howard isomorphism shows: this means that there is a way of mapping formulas and proofs from one system in formulas and proofs of the other one, in such a way that if $p$ is a proof of $F$ from the hypothesis $H_1,\dots,H_n$ the its image $[p]$ is a proof of the image formula $[F]$, image of $F$, from the hypothesis $[H_1],\dots,[H_n]$, images respectively of $H_1,\dots,H_n$.
