Sciweavers

Share
TPHOL
2007
IEEE
9 years 8 months ago
Mizar's Soft Type System
In Mizar, unlike in most other proof assistants, the types are not part of the foundations of the system. Mizar is based on untyped set theory, which means that in Mizar expression...
Freek Wiedijk
TPHOL
2007
IEEE
9 years 8 months ago
Building Formal Method Tools in the Isabelle/Isar Framework
Abstract We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins,...
Makarius Wenzel, Burkhart Wolff
TPHOL
2007
IEEE
9 years 8 months ago
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
Abstract. This paper introduces the logical system HOL2P that extends classical higher order logic (HOL) with type operator variables and universal types. HOL2P has explicit term o...
Norbert Völker
TPHOL
2007
IEEE
9 years 8 months ago
Primality Proving with Elliptic Curves
Laurent Théry, Guillaume Hanrot
TPHOL
2007
IEEE
9 years 8 months ago
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
This paper concerns the formal semantics of programming languages, and the specification and verification of software. We are interested in the verification of real programs, wr...
Tom Ridge
TPHOL
2007
IEEE
9 years 8 months ago
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
Abstract. In this proof pearl, we demonstrate the power of higherorder encodings in the logical framework Twelf[PS99] by investigating proofs about an algorithmic specification of...
Brigitte Pientka
TPHOL
2007
IEEE
9 years 8 months ago
Source-Level Proof Reconstruction for Interactive Theorem Proving
Abstract. Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part...
Lawrence C. Paulson, Kong Woei Susanto
TPHOL
2007
IEEE
9 years 8 months ago
Proof Pearl: De Bruijn Terms Really Do Work
Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (`a la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented ...
Michael Norrish, René Vestergaard
TPHOL
2007
IEEE
9 years 8 months ago
Using XCAP to Certify Realistic Systems Code: Machine Context Management
Formal, modular, and mechanized verification of realistic systems code is desirable but challenging. Verification of machine context management (a basis of multi-tasking) is one ...
Zhaozhong Ni, Dachuan Yu, Zhong Shao
books