title: A question about logic and the Curry-Howard correspondence
body: <p>Could you please explain me what is the basic connection between the fundamentals of logical programming and the phenomenon of syntactic similarity between type systems and conventional logic? </p>