Discussion: Propositions as Types
Before class, add your comments or questions about this CACM article: http://cacm.acm.org/magazines/2015/12/194626-propositions-as-types/fulltext
I would like to get more explanations on Figure 8.
Is this paper an extension of the Curry-Howard correspondence or just a description of it? I am having a hard time finding the novelty of the paper itself.
I am curious how exactly continuation-passing style corresponds to Godel's double-negation translation.
Given that any logic corresponds to a type system, what would a non-monotonic logic correspond to?
If a given logic is inconsistent, does it only imply that the corresponding type system could not terminate. Or can other issue arise?
In what sense is (typed?) lambda calculus a universal model of computation? What notion of computation are we starting with that makes us justified in saying that it is a model of computation? Where does concurrent computation fit in with this paper? Do you need more powerful mathematical models for concurrent computation? What practical impacts for programmers does the CH correspondence have besides the fact that it allows us to prove things about our programs?
Is the transformation of proofs into programs and the evaluation of the programs the way in which proof solvers work? Or is it based on pattern matching logic rules to incrementally explore the area of provable facts?