We present a framework for intensional reasoning in typed -calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a propositions-as-types-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.

Being part of the RoboCup initiative, the RoboCup@Home league targets the development and deployment of autonomous service and assistive robot technology being essential for future personal domestic applications. The domain of domestic service and assistive robotics implicates a wide range of possible problems. The primary reasons for this include the large amount of uncertainty in the dynamic and non-standardized environments of the real world, and the related human interaction. Furthermore, the application orientation requires a large effort towards high level integration (...) combined with a demand for general robustness of the systems. This article details the need for interdisciplinary community effort to iteratively identify related problems, to define benchmarks, to test and, finally, to solve the problems. The concepts and the implementation of the RoboCup@Home initiative as a combination of scientific exchange and competition is presented as an effi cient method to accelerate and focus technological and scientific progress in the domain of domestic service robots. Finally, the progress in terms of performance increase in the benchmarks and technological advancements is evaluated and discussed. Keywords: Domestic Service Robotics, Application, Uncertainty, Benchmark, Competition, Human–Robot Interaction, RoboCup@Home. (shrink)

Within the community of researchers applying type theory to natural language there have been proposals to use contexts from type theory to model information states and to use context extension to model information updates. Examples of this are Ranta (1994) and research conducted in the DenK project (e.g. Ahn, 1995, Ahn and Borghuis, 1998).