Programming Languages

Business- and mission-critical systems are becoming increasingly more complex, and Galois' programming languages research provides insights and techniques to address the problems stemming from this complexity. Whether it be designing domain specific languages, scaling concurrent network services, or tackling design problems in secure systems, our programming language work is influenced by our background in types, semantics, and language design, and is built on functional programming concepts.


We have long been involved in the functional programming community, as sponsors of conferences and open source events (ICFP, Haskell Hackathons), or via material support (we host both the primary Haskell source repository Hackage as well as other community services).  The Commercial Users of Functional Programming workshop series was initiated by Galois to provide a venue for sharing knowledge about the growing use of functional programming in industry. In 2010, Galois' Chief Scientist, John Launchbury, was inducted as an ACM Fellow in recognition of his contributions to the development of functional programming.

Open Source

Much of the code we develop is released back to the community, in the form of patches and libraries for the open source functional programming language Haskell, including,

We are founding members of the Industrial Haskell Group.


Galois Contacts

Aaron Tomb - Research Lead
John Launchbury - Chief Scientist

Read More

  • Launchbury, J. and Elliott, T2010. Concurrent orchestration in Haskell. In Proceedings of the Third ACM Haskell Symposium on Haskell (Baltimore, Maryland, USA, September 30 - 30, 2010). Haskell '10. ACM, New York, NY, 79-90.
  • Browning, S. and Weaver, P. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In Design and Verification of Microprocessor Systems for High-Assurance, David S. Hardin, Editor. Springer 2010
  • Colby Hoffman, Jeff Lewis, Brad Martin, Sally Browning, A Complete Design Flow for MILS in a Single High Assurance FPGA, European Reconfigurable Radio Technologies Workshop, 2010
  • Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. Copilot: A Hard Real-Time Runtime Monitor. To appear in the proceedings of the 1st Intl. Conference on Runtime Verification (RV'2010), 2010. Springer.
  • Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Design Conference, FMCAD'09, Austin, TX, November 2009, IEEE.
  • Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe: Experience report: roll your own real-time simulator. In ACM SIGPLAN Haskell Symposium 2009.
  • Lee Pike: How to pretty-print a long formula. In progress (paper and the pretty-printer are available).
  • Jon Rafkind, Adam Wick, Matthew Flatt, and John Regehr: Precise Garbage Collection for C. ISMM 2009.
  • Lee Pike, Don Stewart, and John Van Enk: Autonomous Verification and Validation (position paper). CPS Week 2009 Workshop on Mixed Criticality

Collaborate with Us

Licensing - Obtain a license for one of our advanced technologies.

Research & Development - Solve your toughest problems by exploring new approaches with us.

Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.

Let's Work TogetherStart the Conversation >>