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.
- Aug 2011: Journal version accepted for publication by JFP!
- Dec 2010: Technical report now available! (Follow the link below)
- 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.
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.