A number of applications based on personal health records (PHRs) are emerging in the field of health care and wellness. PHRs empower patients by giving them control over their hea...
Efficient handling of quantifiers is crucial for solving software verification problems. E-matching algorithms are used in satisfiability modulo theories solvers that handle quant...
Michal Moskal, Jakub Lopuszanski, Joseph R. Kiniry
This note is about work in progress on the topic of "internal type theory" where we investigate the internal formalization of the categorical metatheory of constructive ...
This paper describes the Signature Compiler, which can compile an LF signature to a custom proof checker in either C++ or Java, specialized for that signature. Empirical results a...
In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning technique of logical relations in a case study about equivalence checking. He pr...
In this paper, we describe a proof-theoretic foundation for bottom-up logic programming based on uniform proofs in the setting of the logical framework LF. We present a forward un...
We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refine...
We present a Hoare-style specification and verification approach for invariants in sequential OO programs. It allows invariants over nonhierarchical object structures, in which upd...
Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper,...