# Recitation 22

1. Explain the correspondence between propositions and types. How is each of the following expressed in Coq, and what is a corresponding way of expressing it in OCaml?

• implication
• conjunction
• disjunction

2. Explain the correspondence between proofs and programs. Then, for each of the following propositions, determine its corresponding type in both OCaml and Coq, then write an OCaml and a Coq definition to give a program of that type, as we did above. Your program proves that the type is inhabited, which means there is a value of that type. It also proves the proposition holds.

• $$(p \wedge q) \rightarrow (q \wedge p)$$
• $$(p \vee q) \rightarrow (q \vee p)$$