Research in this area focuses on the design of new formalisms and frameworks to improve the quality of software. Software is a solution to a computational problem using a formal programming language. The constructs of the language and the tools available to model, implement, and test a software system influence the quality of that solution, in terms of correctness, reliability, readability, computational efficiency, and efficiency in design and development. At the linguistic level, research focuses on constructing methods for extending existing languages with domain specific features, for example, and in exploiting logic and type theory based approaches in developing flexible and secure programs. At the implementation level, our work focuses on designing virtual machines and compilation techniques to support extensibility and to realize new and sophisticated programming language features.

Labs and selected projects 

• Abella: An Interactive Theorem Prover for Reasoning About Specifications of Computations Gopalan Nadathur
• CriSys: Critical Systems Research Group Mats Heimdahl
• Flowcheck Stephen McCamant
• MELT: Minnesota Extensible Language Tools Group Eric Van Wyk
• Teyjus: an efficient implementation of Lambda Prolog Gopalan Nadathur

Related centers and programs 

• University of Minnesota Software Engineering Center