Hongwei Xi received his Ph.D. degree in the field of Pure and Applied Logic from Carnegie Mellon University (CMU), Pittsburgh, PA, 1998. He joined the Computer Science Department at Boston University in October 2001.
Dr. Xi's research primarily focuses on applying advanced type theory to modern programming language design and implementation. He is the principal designer and implementer of the ATS programming language, which unleashes the power of types by combining programming with theorem proving.
In the past, Dr. Xi did a large body of pioneering work on supporting dependent types for practical programming and served on the program committees of several prestigious ACM conferences on programming languages. Also, he is a recipient of the NSF CAREER Award.

AG 1, AG 3, AG 5, RG2, AG 2, AG 4, RG1, SWS   Info

Public Audience

English

-- Not specified --

Saarbrücken

ATS is a programming language with a highly expressive type system
rooted in the framework Applied Type System. In particular, both
dependent types and linear types are available in ATS. Also, a variety
of programming paradigms are incorporated into ATS, which include:

1. Functional programming
2. Object-oriented programming
3. Imperative programming (with pointers)
4. Concurrent programming (with pthreads)

In addition, ATS contains a component ATS/LF that supports a form of
(interactive) theorem proving, where proofs are written as total
functions. With this component, we can advocate a programming paradigm
that combines programming with theorem proving. In this talk, we give
an overview of programming with theorem proving in ATS, and also point
out the potential of this programming paradigm in facilitating the
construction of safe and reliable software.

Chad Brown

--email hidden

passcode not visible

logged in users only

Theorem Proving; ATS