We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

We present an innovative satellite-based solar UV (ultraviolet) radiation dosimeter with a mobile app interface that has been validated by exploiting both ground-based measurements and an in vivo assessment of the erythemal effects on some volunteers having controlled exposure to solar radiation. The app with this satellite-based UV dosimeter also includes other related functionalities such as the provision of safe sun exposure time updated in real-time and end exposure visual/sound alert. Both validations showed that the system has a good accuracy and reliability needed for health-related applications. This app will be launched on the market by siHealth Ltd in May 2016 under the name of “HappySun” and is available for both Android and iOS devices (more info on http://www.happysun.co.uk). Extensive R&D activities are on-going for the further improvement of the satellite-based UV dosimeter's accuracy.

We give a sound and complete labelled natural deduction system for a bundled branching temporal logic, namely the until-free version of BCTL*. The logic BCTL* is obtained by referring to a more general semantics than that of CTL*, where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL* validity semantics. We give both a classical and an intuitionistic version of our labelled natural deduction system for the until-free version of BCTL*, and carry out a proof-theoretical analysis of the intuitionistic system: we prove that derivations reduce to a normal form, which allows us to give a purely syntactical proof of consistency (for both the intuitionistic and classical versions) of the deduction system.

Contrary to the classical case, the relation between quantum programming languages and quantum Turing Machines (QTM) has not been fully investigated. In particular, there are features of QTMs that have not been exploited, a notable example being the intrinsic infinite nature of any quantum computation. In this paper, we propose a definition of QTM, which extends and unifies the notions of Deutsch and Bernstein & Vazirani. In particular, we allow both arbitrary quantum input, and meaningful superpositions of computations, where some of them are “terminated” with an “output”, while others are not. For some infinite computations an “output” is obtained as a limit of finite portions of the computation. We propose a natural and robust observation protocol for our QTMs, which does not modify the probability of the possible outcomes of the machines. Finally, we use QTMs to define a class of quantum computable functions—any such function is a mapping from a general quantum state to a probability distribution of natural numbers. We expect that our class of functions, when restricted to classical input-output, will not be different from the set of the recursive functions.

We extend to natural deduction the approach of Linear Nested Sequents and of 2-Sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction: only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (à la Scott) for formulating sound deduction rules.