Explore projects

Interface theories -- construction site --

Metalogical frameworks that extend LF - the Edinburgh Logical Framework. These provide common features - e.g. record types, subtyping, or flexary functions - of logical languages at the meta-level for inheritance in LFX-specified logics.

Template repository for an MathHub/MMT archive. Documents the structure created by lmh when intiializing a repository (modulo archive name and optional config)

The knowledge for integrating the Sage system into the OpenDreamKit virtual Research Environment.

the standard library

Sources included with the FoCaLiZe distribution

Tom's guided research project

The logical foundation(al theories) used by MitM projects

EXPERIMENTAL: Formalizing Mathematical Models as Research Data

INFRASTRUCTURE: the meta information for the Math-in-the-Middle Ontology

meta info for PVS