Curriculum Vitae, Mark Hills

From FSL
Jump to: navigation, search

Urbana-Champaign, IL | |


Research Interests

I am interested broadly in programming languages, formal methods, and software engineering. In general, areas of interest include the following:

  • Rewriting logic semantics and K
  • The application of modularization techniques to language definitions
  • Tool-supported and executable semantics
  • Program analysis (especially static analysis) and program verification
  • Language design, especially as applied to functional and object-oriented languages
  • Formal verification of language semantics using automated theorem proving
  • Models of distributed and concurrent computation
  • Software engineering, including semantics-driven, algebraic, and rewriting based tools and techniques
  • Model-driven engineering

I am also interested in mathematics as it relates to computer science, including category theory and mathematical logic. I am a research assistant in the Formal Systems Laboratory. I was previously with the Parallel Programming Lab, where some of my research involved language support for parallel systems, especially those using an asynchronous message-passing model of communication.

Research Experience

Current Research

The goal of my current research, and the focus of my thesis (which I'm busy writing), is to encourage the use of formal language definitions. I am following a two-pronged approach to this end. First, I am working to make the definitions easier to create by making them more modular, allowing language features to be created once and then leveraged both within different variants of the same language and across different languages. Second, I am working to find ways to best leverage formal language definitions, with the current focus being on using these definitions for type checking and static analysis. Both topics include a combination of theoretical and more applied material. This research takes place within the context of rewriting logic semantics and K, a formalism for defining computation.

Past Research

While in the Parallel Programming Lab, my research was mainly focused on two areas: orchestration languages for asynchronous, message-passing systems, and parallel scientific computing applications using FEM methods with experimental advancing-front algorithms (my focus was on the parallel support for these methods). I am still involved at a low level with this work, but am mainly focused on what is listed above as current research.


Conference and Workshop Publications

Towards a Module System for K
Blank.gifMark Hills and Grigore Rosu
Blank.gifWADT'08, LNCS 5486, pp 187-205. 2009
Blank.gifPDF, LNCS, WADT'08, BIB

A Rewriting Logic Approach to Static Checking of Units of Measurement in C
Blank.gifMark Hills, Feng Chen and Grigore Rosu
Blank.gifRULE'08, ENTCS, to appear, 2008
Blank.gifPDF, RULE'08 slides, RULE'08, BIB

Memory Representations in Rewriting Logic Semantics Definitions
Blank.gifMark Hills
Blank.gifWRLA'08, ENTCS, to appear, 2008
Blank.gifPDF, WRLA'08 slides, WRLA'08, BIB

KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis
Blank.gifMark Hills and Grigore Rosu
Blank.gifRTA'07, LNCS 4533, pp 246-256. 2007
Blank.gifPDF, RTA'07 slides, LNCS, RTA'07, BIB

On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
Blank.gifMark Hills and Grigore Rosu
Blank.gifFMOODS'07, LNCS 4468, pp 107-121. 2007
Blank.gifPDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
Blank.gifMark Hills, Traian Florin Serbanuta and Grigore Rosu
Blank.gifWRLA'06, ENTCS 176(4), pp. 215-231. 2007
Blank.gifPDF, Experiments, ENTCS, WRLA'06, BIB

An Orchestration Language for Parallel Objects
Blank.gifL.V. Kale, Mark Hills and Chao Huang
Blank.gifPDF, PPL Paper Page, LCR'04, BIB

Posters and Doctoral Symposia

A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Blank.gifMark Hills and Grigore Rosu
Blank.gifOOPSLA'07 Companion, ACM Press, pp 827-828. 2007
Blank.gifPDF, OOPSLA'07 poster, ACM, OOPSLA'07, BIB

A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Blank.gifMark Hills and Grigore Rosu
Blank.gifTechnical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
Blank.gifPDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB

An Executable Rewriting Logic Semantics of K-Scheme
Blank.gifPatrick Meredith, Mark Hills and Grigore Rosu
Blank.gif8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
Blank.gifPDF, SCHEME'07, BIB

Technical Reports

Pluggable Policies for C
Blank.gifMark Hills, Feng Chen and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2008-2931, January 2008
Blank.gifPDF, TR@UIUC, BIB

A K Definition of Scheme
Blank.gifPatrick Meredith, Mark Hills and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2007-2907, October 2007
Blank.gifPDF, TR@UIUC, BIB

A Rewriting Based Approach to OO Language Prototyping and Design
Blank.gifMark Hills and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2006-2786, October 2006
Blank.gifPDF, TR@UIUC, BIB

A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages
Blank.gifFeng Chen, Mark Hills and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2006-2702, March 2006
Blank.gifPDF, TR@UIUC, BIB

Automatic and Precise Dimensional Analysis
Blank.gifMarcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2005-2668, December 2005
Blank.gifPDF, Sources, TR@UIUC, BIB

An Executable Semantic Definition of the Beta Language using Rewriting Logic
Blank.gifMark Hills, T. Baris Aktemur and Grigore Rosu
Blank.gifTechnical Report UIUCDCS-R-2005-2650, November 2005
Blank.gifPDF, TR@UIUC, BIB

Teaching Experience

CS421: Programming Languages and Compilers [Summer 2008, Summer 2006]. Instructor for the course. Tasks include preparing and delivering lectures, developing homeworks and tests, working with students to develop appropriate course projects, grading homeworks, tests, and projects, and working with students to provide what I hope to be an effective learning environment. Students include a mix of undergrad, graduate, and online students.

CS422: Programming Language Design [Fall 2007, Fall 2006, Fall 2005, Fall 2004]. Served as a teaching assistant for the course, delivered lecture on several occasions, provided support over the course newsgroup and in one-on-one meetings with students, developed the course project, graded homeworks and project submissions.


  • Student member of Admissions committee, UIUC Department of Computer Science (2009 admissions)
  • Organizational co-chair, AMAST'08
  • PC Chair, ECOOP 2008 Doctoral Symposium
  • Member of Grad Study committee, UIUC Department of Computer Science (Fall 2005-Spring 2007)
  • Organized local programming languages seminar/reading group for UIUC Department of Computer Science (2004-2007)
  • Organized local meeting of the Midwest Society for Programming Languages and Systems (2006)
  • Reviewer for
    • 10th International Conference on Distributed Computing and Networking (ICDCN 2009)
    • 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008)
    • 2008 ECOOP Doctoral Symposium and PhD Student Workshop
    • 8th Workshop on Runtime Verification (RV 2008)
    • 7th International Workshop on Rewriting Logic and its Applications (WRLA 2008)
    • 2nd Conference on Algebra and Coalgebra in Computer Science (CALCO 2007)
    • 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2007)
    • Structural Operational Semantics 2007 (SOS 2007)
    • International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2006)
    • 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006)
    • 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2005)
    • ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005)
    • Journal of Theoretical Computer Science

Professional/Academic Organizations

Member, ACM
Member, IEEE Computer Society
1991-1995, Member WIU Computer Science Association
1994-1995, Member Upsilon Pi Epsilon


Department of Computer Science, University of Illinois Urbana-Champaign

Pursuing a doctor of philosophy in Computer Science since August 2003.

Relevant Course Work

  • CS422: Programming Language Design
  • CS426: Compiler Construction
  • CS475: Formal Models of Computation
  • CS476: Program Verification
  • CS498: Topics in Automated Deduction (Inductive Proof, HOL)
  • CS522: Programming Language Semantics
  • CS524: Foundations of Concurrent Programming Languages and Systems
  • CS526: Advanced Compiler Construction
  • CS576: Topics in Automated Deduction
  • CS598: Advanced Topics in Security
  • CS598: Program Generation


2003 Computer Science Department Fellow, UIUC
2005 Excellent Teaching Assistant Award, for Fall 2004

Department of Computer Science, Western Illinois University

B.S. Computer Science, Minor in Mathematics, May, 1995.
GPA: Overall 4.0 of 4.0, Major 4.0 of 4.0

Relevant Course Work

  • CS271: The Language C
  • CS273: The Language C++
  • CS276: The Language Lisp
  • CS310: Assembly Language Programming
  • CS380: Survey of Programming Languages
  • CS410: Systems Programming
  • CS411: Theory and Techniques of Compilers
  • CS511: Operating Systems I (graduate level)
  • CS548: Artificial Intelligence II (graduate level)


1995 Graduated Summa Cum Laude, Honors Scholar in Computer Science
1995 Computer Science Departmental Scholar
1994,1995 Inforte Outstanding Computer Science Student
1994 Inducted into Upsilon Pi Epsilon Computer Science Honor Society
1992 Inducted into Phi Kappa Phi Honor Society
1992 Inducted into Phi Eta Sigma Freshman Honor Society
1991-1995 Dean's List, College of Applies Sciences
1991-1995 Semester Honors
1995-1995 WIU Foundation Scholarship Award Winner
1991-1994 Illinois General Assembly Tuition Waver
1991-1995 Multiple Other Merit-Based Scholarships

Major Graduate Projects (Course Related)

Course Description
CS 524 (Foundations of Concurrent Programming Languages and Systems) Secure Actors: developed security extensions to a Java-based actor language implementation, including secure communication via SSL, authentication, and role-based authorization for message sends
CS 576 (Topics in Automated Deduction) Formalization of BabyIL: formalize the definition of the BabyIL language using Isabelle. This work is ongoing with Prof. Elsa Gunter.
CS 598 (Advanced Topics in Security) Formalization of Web Services Protocols: formalize a web services based workflow protocol using the TulaFale web services security verification tool; this work is associated with the WSEmail research project under Prof. Carl Gunter


Major Undergraduate Projects (Course Related)

Course Description
CS 548 (Artificial Intelligence II) Adaptive Mutation and Genetic Algorithms: unpublished paper, discusses effects of mutation on the functioning of a genetic algorithm.
CS 548 (Artificial Intelligence II) Neural Network Training Algorithms: A Comparative Analysis: unpublished paper, discussing alternatives to standard backpropagation training of a neural network
CS 460 (Artificial Intelligence I) Genesis & OOGA: Two Approaches to Genetic Algorithm Implementation: unpublished paper, written with Richard Terlep, describing two systems for implementing genetic algorithms, including a discussion of how the systems work and examples of genetic algorithms
CS 380 (Survey of Programming Languages) The DIPL Language: unpublished paper from the Survey of Programming Languages course, describes the syntax and semantics of a new programming language designed specifically for page layout
Independent Study Developed enhancements to the Western Illinois Pretty Printer (WIPP), a printing application used to print source code.
Independent Study Implemented enhancements to the virtual machine used in the CS410 course, System Software, and reimplemented the assembler for this machine in C based on the preexisting Pascal implementation

Industry Experience

Independent Consultant, Chicago, IL
1/2003 - 8/2003
I led technology aspects of packaged software implementation and customization projects, including installation, tuning, environment certification, and custom development. Also, I created custom client applications and custom integration software, optimized databases, and trained system users.

Inforte, Chicago, IL
Manager, Advanced Technology Group 3/1999 - 12/2002
I investigated new technology solutions and new releases of partner software packages. This included developing prototypes of working systems and reusable software components that could then be used by project teams, and sometimes involved working directly with the vendors. This also included developing internal training, working with project teams on initial implementations, and individually mentoring team members.

Inforte, Chicago, IL
Senior Technology Analyst, 1/1998 - 3/1999
I investigated new technologies, especially focused on Microsoft-based technologies such as Windows application development tools, web site development tools, and distributed component models (DCOM/MTS). I also worked with project teams to provide project assistance.

Inforte, Chicago, IL
Consultant, 5/1995 - 12/1998
I worked on custom development and networking projects, and I led small project teams.

Personal tools