Mechanized Semantic Library

The Mechanized Semantic Library is a collection of mathematical techniques useful for developing semantic models of program logics and type systems: separation algebras, permission share models, indirection theory (a clean axiomatization of step indexing), and modal logics. The library has a special emphasis on techniques which integrate smoothly into a mechanical theorem prover; at the moment the library is only available for use in Coq

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element