Yale FLINT Group: Home

Yale FLINT Group: Advanced Development of Certified Software

The FLINT group at Yale aims to develop a novel and practical programming infrastructure for constructing large-scale certified systems software. By combining recent new advances in programming languages, formal semantics, certified operating systems, program verification, proof assistants and automation, language-based security, and certifying compilers, we hope to attack the following research questions:

what system software structures can offer the best support for extensibility, security, and resilience?
what program logics and semantic models can best capture these abstractions?
what are the right programming languages and environments for developing such certified system software?
how to build new automation facilities to make certified software really scale?

Research	An overview of our research agenda.
People	Who we are.
Publications	Published papers, technical reports, and talks online.
Software	Source code available for download.
Support	Research grants that support our work.
Links	Pointers to related projects and resources.
Internal	Restricted access. Information for members, ideas for student projects, etc.

colophon

Contents