Sciweavers

Share
TPHOL
2003
IEEE
10 years 5 months ago
First Order Logic with Domain Conditions
This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. ...
Freek Wiedijk, Jan Zwanenburg
TPHOL
2003
IEEE
10 years 5 months ago
Applications of Polytypism in Theorem Proving
Abstract. Polytypic functions have mainly been studied in the context of functional programming languages. In that setting, applications of polytypism include elegant treatments of...
Konrad Slind, Joe Hurd
TPHOL
2003
IEEE
10 years 5 months ago
A Coverage Checking Algorithm for LF
Coverage checking is the problem of deciding whether any closed term of a given type is an instance of at least one of a given set of patterns. It can be used to verify if a functi...
Carsten Schürmann, Frank Pfenning
TPHOL
2003
IEEE
10 years 5 months ago
Formalizing Hilbert's Grundlagen in Isabelle/Isar
Laura I. Meikle, Jacques D. Fleuriot
TPHOL
2003
IEEE
10 years 5 months ago
MetaPRL - A Modular Logical Environment
MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative p...
Jason Hickey, Aleksey Nogin, Robert L. Constable, ...
TPHOL
2003
IEEE
10 years 5 months ago
Inductive Invariants for Nested Recursion
Abstract. We show that certain input-output relations, termed inductive invariants are of central importance for termination proofs of algorithms defined by nested recursion. Indu...
Sava Krstic, John Matthews
TPHOL
2003
IEEE
10 years 5 months ago
Verified Bytecode Subroutines
Gerwin Klein, Martin Wildmoser
TPHOL
2003
IEEE
10 years 5 months ago
Program Extraction from Large Proof Developments
Abstract. It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time an...
Luís Cruz-Filipe, Bas Spitters
TPHOL
2003
IEEE
10 years 5 months ago
Verifying Second-Level Security Protocols
Abstract. A second-level security protocol is defined as a security protocol that relies on an underlying security protocol in order to achieve its goals. The verification of cla...
Giampaolo Bella, Cristiano Longo, Lawrence C. Paul...
books