Section: Research Program

Extending logical frameworks with logical time

The Curry-Howard isomorphism (proposition-as-types and proofs-as-typed-$\lambda$-terms) represent the logical and computational basis to interactive theorem provers: our challenge is to investigate and design time constraints within a dependent type theory (e.g. if event A happened-before event B, then the timestamp of A is less than the timestamp of B). We hope to extend the Edinburgh Logical Framework (LF) of Harper-Honsell-Plotkin with relevant constructs expressing logical time and synchronization between processes. Also, union and intersection types with their subtyping constraints theories could capture some CCSL constraints needed to formalize logical clocks (in particular CCSL expressions like subclock, clock union, intersection and concatenation) and provide opportunities for an ad hoc polymorphic type theory. Logical time constraints seen as property types can be beneficially handled by logical frameworks. The new challenge here is to demonstrate the relevance of type theory to work on logical and multiform timing constraint resolution.