Iris recognition is one of the most powerful techniques for biometric identification ever developed. Commercial systems based on the algorithms developed by John Daugman have been available since 1995 and have been used in a variety of practical applications. However, all currently available systems impose substantial constraints on subject position and motion during the recognition process. These constraints are largely driven by the image acquisition process, rather than the particular pattern-matching algorithm used for the recognition process. In this paper we present results of our efforts to substantially reduce constraints on position and motion by means of a new image acquisition system based on high-resolution cameras, video synchronized strobed illumination, and specularity based image segmentation. We discuss the design tradeoffs we made in developing the system and the performance we have been able to achieve when the image acquisition system is combined with a standard iris recognition algorithm. The Iris on the Move (IOM) system is the first system to enable capture of iris images of sufficient quality for iris recognition while the subject is moving at a normal walking pace through a minimally confining portal

An interactive graphical environment for supporting the development and use of Haskell applications programs is described. The environment, named Vital, is particularly intended for supporting the open-ended, incremental development style often preferred by non-specialist users in which successive steps of program development are motivated and informed by results so far obtained.Significant features of Vital include: the graphical display of data structures in a format defined by a datatype-indexed stylesheet, the way that evaluation of (possibly infinite) values is demand-driven by the action of the user scrolling around an unbounded workspace, and support for copy-and-paste graphical editing of data structures. This latter allows, for example, the user to modify a complex data structure by point-and-click operations, or to create (by functional evaluation) a regular data structure and then edit values or expressions into it. The effect of each editing operation is immediately reflected in the Haskell program source code.

This paper discusses the principles of implementing an LCF-style proof assistant using a purely functional metalanguage. Two approaches are described; in both, signatures are treated as ordinary values, rather than as mutable components within an abstract datatype. The first approach treats the object logic as a partial algebra and represents it as a partial datatype, that is, a datatype in which the domains of the constructors are restricted by predicate functions. This results in a compact, executable specification of the logic. The second approach uses an abstract type to allow an efficient representation of the logic, whilst keeping the same interface. A case study describes how these principles were put into practice in implementing a fairly complex dependently-sorted logic.

VERITAS/sup +/, a specification logic based on dependent types, is described. The overall aim is to demonstrate how the use of dependent types together with subtypes and datatypes allows the writing of specifications that are clear, concise, and generic. The development of theories of arithmetic, numerals, and iterative structures is described, and the proof of a theorem that greatly simplifies the formal verification of iterative arithmetic structures is outlined. The VERITAS/sup +/ logic is defined by modeling it as a partial algebra within a purely functional metalanguage. Aspects of the computational implementation of the logic and its associated toolset are briefly described.>