Chucky Ellison

From FSL
Revision as of 23:30, 10 June 2013 by Celliso2 (Talk | contribs)

Jump to: navigation, search

Former student of Grigore Rosu; I graduated in 2012.



I am interested in programming language semantics, type systems, reflection (semantics and safety), coinduction, and automated reasoning. I'm currently focusing on giving a complete formal semantics to the C programming language. This current state of the project can be found on our public Google Code project. Additionally, we have a POPL'12 paper:

An Executable Formal Semantics of C with Applications
Chucky Ellison and Grigore Rosu
POPL'12, ACM, pp 533-544. 2012
Abstract. This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker "for free". The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.
PDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB

Eventually, this will be integrated with Matching Logic, a program verification logic and verification tool for imperative languages:

Matching Logic: An Alternative to Hoare/Floyd Logic
Grigore Rosu, Chucky Ellison and Wolfram Schulte
AMAST'10, LNCS 6486, pp 142-162. 2010
Abstract. This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP's Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.
PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB

In the past, I also worked on defining and analyzing type systems using a rewriting-based style:

A Rewriting Logic Approach to Defining Type Systems
Chucky Ellison
Master's Thesis

Abstract. We show how programming language semantics and definitions of their corresponding type systems can both be written in a single framework amenable to proofs of soundness. The framework is based on full rewriting logic (not to be confused with context reduction or term rewriting), where rules can match anywhere in a term (or configuration).

We present an extension of the syntactic approach to proving type system soundness presented by Wright and Felleisen [1994] that works in the above described semantics-based domain. As before, the properties of preservation and progress are crucial. We use an abstraction function to relate semantic configurations in the language domain to semantic configurations in the type domain, and then proceed to use the preservation and progress properties as usual. We also develop an abstract type system, which is a type system modulo certain structural characteristics.

To demonstrate the method, we give examples of five languages and corresponding type systems. They include two imperative languages and three functional languages, and three type checkers and two type inferencers. We then proceed to prove that preservation holds for each.


A Rewriting Logic Approach to Type Inference
Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
WADT'08, LNCS 5486, pp 135-151. 2009
Abstract. Meseguer and Roșu proposed rewriting logic semantics (RLS) as a programing language definitional framework that unifies operational and algebraic denotational semantics. RLS has already been used to define a series of didactic and real languages, but its benefits in connection with defining and reasoning about type systems have not been fully investigated. This paper shows how the same RLS style employed for giving formal definitions of languages can be used to define type systems. The same term-rewriting mechanism used to execute RLS language definitions can now be used to execute type systems, giving type checkers or type inferencers. The proposed approach is exemplified by defining the Hindley-Milner polymorphic type inferencer \mathcal{W} as a rewrite logic theory and using this definition to obtain a type inferencer by executing it in a rewriting logic engine. The inferencer obtained this way compares favorably with other definitions or implementations of \mathcal{W}. The performance of the executable definition is within an order of magnitude of that of highly optimized implementations of type inferencers, such as that of OCaml.
PDF, Slides(PDF), LNCS, WADT'08, BIB

Additional Information

Curriculum Vitae


Formal Systems Laboratory
Department of Computer Science
University of Illinois at Urbana-Champaign

Contact Data

Personal tools