Sciweavers

TPHOL
2005
IEEE
14 years 5 months ago
Alpha-Structural Recursion and Induction
The nominal approach to abstract syntax deals with the issues of bound names and α-equivalence by considering constructions and properties that are invariant with respect to permu...
Andrew M. Pitts
TPHOL
2005
IEEE
14 years 5 months ago
From PSL to LTL: A Formal Validation in HOL
Using the HOL theorem prover, we proved the correctness of a translation from a subset of Accellera’s property specification language PSL to linear temporal logic LTL. Moreover,...
Thomas Tuerk, Klaus Schneider
TPHOL
2005
IEEE
14 years 5 months ago
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
We discuss methods for dealing effectively with let-bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translatio...
Michael Norrish, Konrad Slind
TPHOL
2005
IEEE
14 years 5 months ago
Verifying a Secure Information Flow Analyzer
Abstract. Denotational semantics for a substantial fragment of Java is formalized by deep embedding in PVS, making extensive use of dependent types. A static analyzer for secure in...
David A. Naumann
40
Voted
TPHOL
2005
IEEE
14 years 5 months ago
Real Number Calculations and Theorem Proving
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem provin...
César Muñoz, David Lester
TPHOL
2005
IEEE
14 years 5 months ago
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2
Francisco-Jesús Martín-Mateos, Jos&e...
TPHOL
2005
IEEE
14 years 5 months ago
A Design Structure for Higher Order Quotients
The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, whe...
Peter V. Homeier