Education
Work Experience
Teaching Experience
Honors
Invited Talks on
Logic Programming and Theorem Proving:
Technical Skills
Conference of the European Association for Computer Science Logic (CSL), Logic Programming Synthesis and Transformation (LOPSTR), Extensions of Logic Programming (ELP), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000).
Publications
Logic
Aircraft Scheduling
References
Statement of Research Interest
My interests revolve around the design of software tools to support automated reasoning, namely in the development and extension of high-level languages and frameworks to make easier automated theorem-proving activities. My current research lies at the intersection of logical frameworks and logic programming. A logical framework is a uniform meta-language and environment, which supports specification, implementation, and formal reasoning about programming languages and logics. It allows discovering the basic principles of programming language design and to experiment with them through implementations and environments. Applications lie in the prototyping of novel programming languages features, as well as in safety architectures for mobile code based on the proof-carrying code paradigm. My current and future work consists mainly in improving the expressive power of those frameworks in order to capture more language phenomena in a concise and natural way; at the same time the goal is to preserve its deign principles, in particular its intentional weakness, which allows practical proof-search, unification and type reconstruction algorithms. A fundamental issue is the representation techniques: they have to be as succinct as possible without losing adequacy. One well-known example is the usage of higher-order abstract syntax. The better the representation the more the meta-theory that can be specified and proved.
In particular, my dissertation "Elimination of Negation in a Logical Framework", addresses the issue of adding negation to a logical frameworks. Some frameworks such as hereditary Harrop formulae and LF also admit a (higher-order) logic programming interpretation, either directly or via the Howard-Curry isomorphism. Nevertheless, this entails that only positive information can be encoded. The user must explicitly program negative predicate definitions, a task that is often tedious, error prone and therefore a good candidate for mechanization. Unfortunately the way in which logic programming has dealt with this issue, namely negation-as-failure is unsuited to our purposes, as its intrinsic operational nature would spoil the adequacy of representations. A different approach has been explored for Horn logic, the so-called transformational one: roughly, it consists of automatically synthesizing an equivalent positive axiomatization of predicates occurring negatively in a (logic) program. The adoption of this paradigm in logical frameworks entails two non-trivial extensions:
The first issue requires the introduction of a strict (relevant)
lambda-calculus, where we can express the question of whether a given function
depends on its argument, which is fundamental when complementing terms
with a binding operator. Technically, this strict calculus is peculiar
in the usage of vacuous variables, which are of independent interest in
the study of substructural logics [2,3].
The second issue is solved by restricting ourselves to an elegant and expressive fragment of hereditary Harrop formulae where static and dynamic assumptions cannot overlap [1]. This makes clause complementation feasible and turns out to be adequate for most applications in logical frameworks. Semantically, this requires a middle ground between the Closed World Assumption associated to Horn logic and the Open World Assumption typical of languages with embedded implication. We call this the Regular World Assumption, which turns out to be a central tool in the meta-theorem proving in Logical Frameworks.
In the future I plan to test the usefulness of elimination negation in the mechanized verification of operational semantics of programming languages and in topics in process algebra such as mutual exclusion. Theoretically, I will generalize the idea of negation elimination from the simply to the dependently typed case. Moreover, this technique applies to other resource-sensitive logical framework, as the ones based on relevant or linear logics. The ability to freely use negation will greatly empower imperative logic programming. An even more ambitious future goal is the definition of an annotated logical framework that can subsume any substructural logic that obeys some basic algebraic properties of annotations. On the logic programming front, I plan to extend negation elimination to full LambdaProlog, by using a suitable formulation of Stuckey's constructive negation via constraints.
Some of my previous research (in collaboration with Mario Ornaghi) [4,5,6,8] is based on the notion of regularity as a basis for logic programming. Basically, regularity abstracts over the good proof-theoretic property of SLD-resolution, in particular the existence of a most general proof tree. I have shown that every logic that can be presented in terms of axiom-application rules (an abstraction of backchaining) and which is regular has the same proof search of Prolog-like languages. Moreover, I have investigated how it is possible to regularize non-regular logics as SLDNF-resolution via source-to-source transformations. The proof-theoretic view of logic programs has also provided a way to simplify and generalize well-known program transformation techniques as partial evaluation and fold/unfold transformations [4].
I also have an active interest in improving the quality and effectiveness
of teaching via computer assistance. At Carnegie Mellon, I have been involved
in the construction and management of the CMU Proof Tutor, a completely
self-paced curriculum of introduction to logic, which replaces Suppes'
VALID program.