MAVIS: A Secure Formal Computational Paradigm based on the Mammalian Visual System

Constructive type theory (CTT) is both a formal logic and a programming language which contains inherent benefits both in terms of formality and program correctness and in the potential for efficient concurrent execution. In contrast, the mammalian visual cortex represents a naturally occurring visual processing system capable of the rapid concurrent evaluation of complex data domains. The efficient exploitation of a merger between these two systems would represent major advantages in such diverse fields as machine reading, automated guidance, navigation and, significantly, biometrically based security identification systems. The current paper explores the possibilities of achieving such a merger and the technological challenges and opportunities it would represent in constructing a practical remote biometric based identification system.