Dminor
Dminor

Dminor is a first-order functional language with the novel combination of the ideas of refinement type and type-test. It can express a rich variety of typing idioms and has a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The type checker uses an SMT Solver to compute subtyping efficiently.

People

News

  • Aug 2011: Journal version accepted for publication by JFP!
  • Dec 2010: Technical report now available! (Follow the link below)
Publications
  • Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy, Semantic Subtyping with an SMT Solver, no. MSR-TR-2010-99, December 2010
  • Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy, Semantic Subtyping with an SMT Solver, in Proceedings of 15th ACM SIGPLAN International Conference on Functional Programming, Association for Computing Machinery, Inc., September 2010
Downloads

Further resources

Some resources for Dminor, developed in Microsoft Research, and formerly known as Minim.

  • The Readme for the Dminor download, available here, contains Dminor samples and listings of Dminor's output.
  • A screencast (from June 2009) comparing the Dminor and M typecheckers is here.
  • The Coq formalization is available here (zip file).
  • There were talks about Dminor at RADICAL 2010 (video, slides) and ICFP 2010 (video, slides).
  • The DVerify project at Saarland University has produced an alternative theorem-proving backend for Dminor, based on the Boogie system.

Some resources for the "M" Modeling Language, developed in Microsoft SQL Server.

  • The code name "M" modeling language as described at Microsoft PDC 2009 is here.
  • The current version of the "M" Language Specification is here.
  • The future of "M" itself is uncertain, according to this MSDN announcement.