ENTCS
2008
13 years 5 months ago
2008
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...
ENTCS
2008
13 years 5 months ago
2008
Efficient handling of quantifiers is crucial for solving software verification problems. E-matching algorithms are used in satisfiability modulo theories solvers that handle quant...
ENTCS
2008
13 years 5 months ago
2008
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 ...
ENTCS
2008
13 years 5 months ago
2008
ENTCS
2008
13 years 5 months ago
2008
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...
ENTCS
2008
13 years 5 months ago
2008
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...
ENTCS
2008
13 years 5 months ago
2008
ENTCS
2008
13 years 5 months ago
2008
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...
ENTCS
2008
13 years 5 months ago
2008
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...
ENTCS
2008
13 years 5 months ago
2008
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...