Serwis Infona wykorzystuje pliki cookies (ciasteczka). Są to wartości tekstowe, zapamiętywane przez przeglądarkę na urządzeniu użytkownika. Nasz serwis ma dostęp do tych wartości oraz wykorzystuje je do zapamiętania danych dotyczących użytkownika, takich jak np. ustawienia (typu widok ekranu, wybór języka interfejsu), zapamiętanie zalogowania. Korzystanie z serwisu Infona oznacza zgodę na zapis informacji i ich wykorzystanie dla celów korzytania z serwisu. Więcej informacji można znaleźć w Polityce prywatności oraz Regulaminie serwisu. Zamknięcie tego okienka potwierdza zapoznanie się z informacją o plikach cookies, akceptację polityki prywatności i regulaminu oraz sposobu wykorzystywania plików cookies w serwisie. Możesz zmienić ustawienia obsługi cookies w swojej przeglądarce.
Inductive type theories, as used in systems like Coq or Lego [11,14,4], provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions. Recursive computation is described by reduction rules, included in the type system under the name ι-reduction. If t is an element of a recursive type, f is a recursive function over that type and v is...
This article describes a set of derived inference rules and an abstract reduction machine using them that allow the inplementation of an interpreter for HOL terms, with the same complexity as with ML code. The latter fact allows us to use HOL as a computer algebra system in which the user can implement algorithms, provided he proved them correct.
This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results confirm the effectiveness of the compression scheme.
We provide a proof using HOL and SPIN of convergence for the Routing Information Protocol (RIP), an internet protocol based on distance vector routing. We also calculate a sharp realtime bound for this convergence. This extends existing results to deal with the RIP standard itself, which has complexities not accounted for in theorems about abstract versions of the protocol. Our work also provides...
Families of inductive types defined by recursion arise in the formalization of mathematical theories. An example is the family of term algebras on the type of signatures. Type theory does not allow the direct definition of such families. We state the problem abstractly by defining a notion, strong positivity, that characterizes these families. Then we investigate its solutions. First, we construct...
The Airborne Information for Lateral Spacing (AILS) program at NASA Langley Research Center aims at giving pilots the information necessary to make independent approaches to parallel runways with spacing down to 2500 feet in Instrument Meteorological Conditions. The AILS concept consists of accurate traffic information visible on the navigation display and an alerting algorithm which warns the crew...
In some ways, microprocessor design quality has improved tremendously since the’ 70’s and’ 80’s. It was not uncommon in those days to have to respin silicon five or ten times before the device exhibited even basic functionality. Microprocessors were designed by circuit designers directly into schematics, with little pre-silicon functional testing. In the late’ 80’s, register transfer level (RTL) descriptions...
We describe a low-level proof format, which can be used for independent proof checking and as an intermediate language for translating proofs between systems. The checker is presented as a virtual machine and the proof format as the bytecode. We compare HOL and Coq with a view to designing this pivot language, and describe a prototype which converts recorded HOL proofs into this intermediate format,...
We verify within the Coq proof assistant that ML typing is sound with respect to the dynamic semantics. We prove this property in the framework of a big step semantics and also in the framework of a reduction semantics. For that purpose, we use a syntax-directed version of the typing rules: we prove mechanically its equivalence with the initial type system provided by Damas and Milner. This work is...
Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical є and δ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real...
We modify the reflection method to enable it to deal with partial functions like division. The idea behind reflection is to program a tactic for a theorem prover not in the implementation language but in the object language of the theorem prover itself. The main ingredients of the reflection method are a syntactic encoding of a class of problems, an interpretation function (mapping the encoding to...
Two methods of programming BDD-based symbolic algorithms in the Hol98 proof assistant are presented. The goal is to provide a platform for implementing intimate combinations of deduction and algorithmic verification, like model checking. The first programming method uses a small kernel of ML functions to convert between BDDs, terms and theorems. It is easy to use and is suitable for rapid prototying...
In this paper we present a library of transcendental functions such as exp, log, cos, sin and tan and also an automated continuity checker for real valued functions, both done using PVS. Our aim is to develop theorem proving support for computer algebra systems, and other applications which rely on mathematical analysis. The focus of the paper is on the actual development done in PVS.
This paper outlines a formal model of the Intel IA-64 architecture, and explains how this model can be used to verify the correctness of assembly-level code optimizations. The formalization and proofs were carried out using the HOL Light theorem prover.
The IA-64 architecture defers floating point and integer division to software. To ensure correctness and maximum efficiency, Intel provides a number of recommended algorithms which can be called as subroutines or inlined by compilers and assembly language programmers. All these algorithms have been subjected to formal verification using the HOL Light theorem prover. As well as improving our level...
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and computationally intensive domain-specific proof procedures. The generality of tactic provers has a performance penalty; the speed of proof search lags far behind special-purpose provers. We present a new modular proving...
We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and—unlike previous approaches using HOAS—at the same time uses the built-in higher-order logic of the theorem prover to formulate specifications. We give examples of verifications, extending those given in [1], that have been...
The purpose of this paper is to describe a “grand logic”, that is, a system of higher order logic capable of use as a general purpose foundation for mathematics. This logic has developed as the logic of a theorem proving system which has had a number of names in its career (EFTTP, Mark2, and currently Watson), and the suitability of this logic for computer-assisted formal proof is an aspect which...
This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating...
Podaj zakres dat dla filtrowania wyświetlonych wyników. Możesz podać datę początkową, końcową lub obie daty. Daty możesz wpisać ręcznie lub wybrać za pomocą kalendarza.