From the point of view of logic, every computation is a deduction from initial premises in a suitable associated formal system. From the point of view of Computer Science, every deduction is an execution sequence of a computation with the premises as initial data. The “Greats” (Brouwer, Kolmogorov, Goedel) raised in the 1930’s a complex of fundamental questions of explicit logic which we can now characterize as determining the exact relation between deduction and computation. One such fundamental relation, stemming from the consistency proofs of Gentzen, has already become a cornerstone of Computer Science. This is the Curry-Howard Isomorphism between typed lambda-terms and intuitionistic deductions.
The Curry-Howard Isomorphism does not of itself capture the self-referential mechanisms available in deductions in sufficiently rich formal systems and in programming languages. Our discovery of a natural system of self-referential proof terms, which we call “proof polynomials”, was essential in our solution to the famous open problem of Goedel (1933) concerning formalization of provability (cf. major scientific accomplishments). Proof polynomials considerably extend the Curry-Howard Isomorphism and lead to a joint calculus of propositions and proofs which unifies several previously unrelated areas. We will explain our solution, and why it changes our conception of the appropriate syntax and semantics for typed programming languages, automated deduction and formal verification, reasoning about knowledge, nonmonotonic reasoning.
Work in progress:
- Reflective lambda-calculus which matches the power of proof polynomials. So far, we have succeeded in building the reflective lambda-calculus (confluent and strongly normalizable) for the core underlying system based on the intuitionistic propositions with implication and conjunction. Next steps here: to capture universal quantifiers, disjunction, classical logic, second order abstraction.
- Building feasible reflection in Nuprl and related systems. An ability of a language to talk about its own objects (sentences, types, proofs) is an essential component of its expressive power. In order to catch up with the conciseness of human reasoning a formal deductive system should have a tractable reflection mechanism. Traditional Goedel numbering is notoriously inefficient and cannot be implemented without principal reconstruction which constitute a challenging theoretical and practical problem.
- Explicit extensibility mechanism for verification systems. A typical problem of verification is to establish a fact F by means of a given formal system V by verifying in V that a certain construction D is a proof of F. Such a scheme necessarily needs a reflection rule of the sort: “D is a proof of F” yields F. The traditional (implicit) reflection does not fit here: the formal verification with the implicit reflection rule is impossible since the justification of such a rule takes the “reflection tower” of theories of increasing proof-theoretical strength well beyond V. In turn, the explicit reflection is provable inside the system, which allows circumventing the “reflection tower” and provides the desired justification of verification.
- Logics of knowledge with justifications, where the atoms “F is known” are replaced by the more informative “t is an evidence of F“. The desire to have such explicit epistemic systems has been repeatedly mentioned by the experts in the corresponding fields of Artificial Intelligence and knowledge representation.
- Explicit provability systems for the higher order theories which presumably provide the provability semantics for the polymorphic second order lambda-calculus. Explicit provability semantics for Girard’s system F and the Matrin-Lof type theory ITT.
- Explicit non-monotonic reasoning on the basis of the explicit modal logic; the goal here is to find a concise non-monotonic logic that subsumes all major non-monotonic systems
In particular, I am working within the Cornell University PRL-team (R. Constable) on the reflection mechanism design for the next generation Nuprl style automated problem-solving systems (Nurpl 5 and MetaPrl). The current system is Nuprl 4, a 200,000-line Lisp-ML hybrid. It is being used for circuit synthesis; program language semantics; and formal verification; as accumulated database of mathematical knowledge. The system now ranks as one of the major tactic-oriented theorem provers.