The goal of the POP group is to understand, develop, and
demonstrate the principles, processes, and supporting technologies for
the construction of computing systems. Special areas of interest
include: applications of logic (including formal semantics and type
theory); techniques for designing and implementing programming
languages; formal specification and verification of hardware and
software systems. A distinguishing characteristic of the POP group is
that it applies formal principles to problems of realistic scale and
complexity, for example: automatic verification of large-scale
commercial hardware systems; implementation of high-speed network
communication software in the ML language; application of
type-theoretic principles in the construction of realistic compilers.
ArchJava:
The ArchJava language integrates a specification of software architecture
into Java source code, and uses a type system to verify that all
run-time communication obeys architectural constraints.
Composable
Software Systems: Providing a scientific and engineering basis for
designing, building, and analyzing composable software systems, and
providing languages, tools, environments, and techniques to support
these activities.
ConCert:
The ConCert Project investigates the theoretical and engineering
basis for the trustless dissemination of software in an untrusted
environment. To make this possible the project investigates
machine-checkable certificates of compliance with security, integrity,
and privacy requirements. Such checkable certificates allow participants
to verify the intrinsic properties of disseminated software, rather
than extrinsic properties such as the software's point of origin.
Formal
Methods: The development and use of mathematically-based
languages, techniques, and tools to support the specification and
verification of software and hardware systems.
Logical Frameworks: The LF
logical framework and its implementation in Twelf constraint logic programming
language and theorem prover.
Logics
of Types and Computation: Using type theory (and topos theory) via realizability to model a constructive logic which accomodates standard types and domain theory, has extensive closure conditions, and supports polymorphism.
Fox: Advancing the
art of programming-language design and implementation, and simultaneously
applying principles of programming languages to advance the art of
systems building, as demonstrated by the
FoxNet.
MESS:
Semantics-based implementation of programming languages.
Model Checking:
Formally verifying finite-state concurrent systems, with applications
to several complex industrial systems such as the Futurebus+
and the PCI local bus protocols.
Scandal: The development of a portable, interactive
environment for programming a wide range of supercomputers, including
the portable, parallel language
NESL and fast implementations of parallel algorithms for
irregular problems.
PSciCo (Parallel
Scientific Computing): Studying how features of advanced programming
languages can be used in the design of algorithms for Scientific and
Geometric computing.
SeLF: Distributed System Security via Logical Frameworks.
