Roberto Virga

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

 

Research interests

Programming languages theory, design and implementation. Higher-order logic, automated theorem proving, applications of rewriting techniques, constraint logic programming.

Programming skills

Education

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

Work experience

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.

Research experience

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.

Teaching experience

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.

Publications

"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)

Miscellaneous

References

Dr. Frank Pfenning, Senior Research Scientist
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15217-3891
Email: fp@cs.cmu.edu
Phone: (412) 268-6343
Fax: (412) 268-5576
Dr. Robert Harper, Associate Professor
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15217-3891
Email: rwh@cs.cmu.edu
Phone: (412) 268-3675
Fax: (412) 268-5576
Dr. Richard Statman, Professor
Department of Mathematical Sciences
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15217-3891
E-mail: statman@cs.cmu.edu
Phone: (412) 268-8475
Fax: (412) 268-6380