Curriculum Vitae, Mark Hills

From FSL

Jump to: navigation, search

Urbana-Champaign, IL | mhills@uiuc.edu | http://www.uiuc.edu/~mhills

Contents

[edit] 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.


[edit] Research Experience

[edit] 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.

[edit] 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.

[edit] Publications

[edit] Conference and Workshop Publications

Towards a Module System for K
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifWADT'08, LNCS, to appear. 2008
Image:blank.gifPDF, WADT'08, BIB

A Rewriting Logic Approach to Static Checking of Units of Measurement in C
Image:blank.gifMark Hills, Feng Chen and Grigore Rosu
Image:blank.gifImage:New.gif RULE'08, ENTCS, to appear, 2008
Image:blank.gifPDF, RULE'08 slides, RULE'08, BIB

Memory Representations in Rewriting Logic Semantics Definitions
Image:blank.gifMark Hills
Image:blank.gifImage:New.gif WRLA'08, ENTCS, to appear, 2008
Image:blank.gifPDF, WRLA'08 slides, WRLA'08, BIB

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

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

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

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


[edit] Posters and Doctoral Symposia

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

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

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


[edit] Technical Reports

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

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


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

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

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


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


[edit] 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.

[edit] Service

  • 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

[edit] Professional/Academic Organizations

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

[edit] Education

[edit] Department of Computer Science, University of Illinois Urbana-Champaign

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

[edit] 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

[edit] Honors

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

[edit] 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

[edit] 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)

[edit] Honors

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

[edit] 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

==

[edit] 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

[edit] 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.

Retrieved from "http://fsl.cs.uiuc.edu/index.php/Curriculum_Vitae%2C_Mark_Hills"
Views