Department of Mathematical Sciences | Office: (412) 268-3337 |
Carnegie Mellon University | Fax: (412) 268-5576 |
5000 Forbes Ave. | Home: (412) 802-7925 |
Pittsburgh, PA 15213 | E-mail: rvirga+@cs.cmu.edu |
Home page: http://www.cs.cmu.edu/~rvirga |
Programming languages theory, design and implementation. Higher-order logic, automated theorem proving, applications of rewriting techniques, constraint logic programming.
Fall 1992 - Summer 1999 Carnegie Mellon University, Pittsburgh, PA
- MS. Mathematics, December 1994
- Ph.D. in Pure and Applied Logic, June 1999 (expected)
- Advisor: Frank Pfenning
- Thesis: Higher-Order Rewriting with Dependent Types (abstract)
Fall 1985 - Spring 1990 University of Milan, Milan, Italy
BS. Computer Science, GPA 9.8/10
Fall 1997 - Summer 1998 Information Discovery, Inc., Los Angeles, CA
Developed artificial-intelligence tools for data mining and pattern visualization of large Oracle/Sybase database warehouses.
Winter 1998 - Spring 1999 Carnegie Mellon University, Pittsburgh, PA
Investigated a CLP(Q)-style extension to the TWELF logical framework to handle equalities and inequalities over numbers. Developed a constraint-solver based on the simplex method.
Spring 1990 - Summer 1992 University of Milan, Milan, Italy
Worked on ENProver, an automated theorem prover based on rewriting techniques. Used Mathematica to develop a theorem prover for first order logic based on an extension of Grobner basis completion.
Financial support from the european research project ESPRIT-KWICK.
Fall 1993 - Spring 1997 Carnegie Mellon University, Pittsburgh, PA
Teaching assistant for several undergraduate courses offered by the Mathematical Sciences department, including: Introduction to Modern Mathematics, Discrete Mathematics, Calculus II, Calculus in Three Dimensions.
Fall 1991 - Spring 1992 National Research Council, Palermo, Italy
Course Instructor on programming using Mathematica.
"Higher-Order Superposition for Dependent Types", Proceedings of the 7th International Conference On Rewriting Techniques and Applications, August 1996 (an extended version has also been published as technical report CMU-CS-95-150)
|
|
|