This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent cubical set model. enables new ways reason about identity types, for instance, function extensionality provable the system. Further, Voevodsky's univalence axiom this We also explain extension with some higher inductive types like circle and propositional truncation. Finally we provide semantics constructive meta-theory.

We present a model of type theory with dependent product, sum, and identity, in cubical sets. describe universe and explain how to transform an equivalence between two types into equality. We also how to propositional truncation the circle. While not expressed internally theory, is constructive metalogic. Thus it step towards computational interpretation Voevodsky's Univalence Axiom.

We introduce Deep500: the first customizable benchmarking infrastructure that enables fair comparison of plethora deep learning frameworks, algorithms, libraries, and techniques. The key idea behind Deep500 is its modular design, where factorized into four distinct levels: operators, network processing, training, distributed training. Our evaluation illustrates (enables combining different codes) (uses carefully selected metrics). Moreover, fast (incurs negligible overheads), verifiable...

Cubical type theory provides a constructive justification to certain aspects of homotopy such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. paper describes semantics, expressed presheaf topos with suitable structure inspired by cubical sets, some higher inductive types. It also extends syntax for types spheres, torus, suspensions, truncations, pushouts. All these are justified...

This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent cubical set model. enables new ways reason about identity types, for instance, function extensionality provable the system. Further, Voevodsky's univalence axiom this We also explain extension with some higher inductive types like circle and propositional truncation. Finally we provide semantics constructive meta-theory.

A central aspect of robotic motion planning is collision avoidance, where a multitude different approaches are currently in use. Optimization-based one method, that often heavily relies on distance computations between robots and obstacles. These can easily become bottleneck, as they do not scale well with the complexity or environment. To improve performance, many methods suggested to use primitives, i.e. simple shapes approximate more complex rigid bodies, simpler compute distances from....

Cubical type theory is an extension of Martin-Löf recently proposed by Cohen, Coquand, Mörtberg, and the author which allows for direct manipulation n-dimensional cubes where Voevodsky’s Univalence Axiom provable. In this paper we prove canonicity cubical theory: any natural number in a context build from only name variables judgmentally equal to numeral. To achieve formulate typed deterministic operational semantics employ computability argument adapted presheaf-like setting.

In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference types for proofs programs (TYPES 2013), Leibniz proceedings informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs.TYPES.2013.107 . http://drops.dagstuhl.de/opus/volltexte/2014/4628 ) Huber (A sets....

We present an interpretation of a version dependent type theory where is interpreted by Kan semisimplicial set. This interprets only weak notion conversion similar to the one used in first published Martin-Löf theory. Each truncated this model can be carried out internally theory, and we have formalized level, which enough represent isomorphisms algebraic structure as equality.

Teams that regularly step back from action and deliberately reflect on their performance strategies show higher performance. Ad hoc emergency teams with changing team composition cannot develop such habits but may engage in short postaction reflection to discuss shortcomings of past potential adaptations for future similar tasks. This study aimed test the effect a self-led reflective briefing resuscitation simulator setting terms three parameters: hands-on time, coordination between chest...

Teleoperating robotic arms is a challenging task that requires years of training to master. It mentally demanding, as the operator must internally compute transformations, or rely on muscle memory, perform even simplest tasks. Alternative methods embodiment –the immersive, first person experience controlling robot from its point view are recently becoming more popular, thanks emergence mixed reality devices. These create an intuitive by tracking users motions, and retargetting them robot....

Identifying the closest fog node is crucial for mobile clients to benefit from computing. In this paper, we analyze performance of Meridian and Vivaldi network coordinate systems task. To that end, simulate a dense environment with clients. We find while really nodes in close proximity, purely latency-oriented identification approach ignores larger problem balancing load across nodes.

Robotic systems are routinely used in the logistics industry to enhance operational efficiency, but design of robot workspaces remains a complex and manual task, which limits system's flexibility changing demands. This paper aims automate workspace by proposing computational framework generate budget-minimizing layout selectively placing stationary robots on floor grid, includes robotic arms conveyor belts, plan their cooperative motions sort packages from given input output locations. We...

We present an algorithmic approach to designing animatronic figures - expressive robotic characters whose movements are driven by a large number of actuators. The input our design system provides high-level specification the space motions character should be able perform. output consists fully functional mechatronic blueprint. cast task as search problem in vast combinatorial possible solutions. To find optimal this space, we propose efficient best-first algorithm that is guided admissible...

We present a domain model of dependent type theory and use it to prove basic metatheoretic properties. In particular, we that two convertible terms have the same Böhm tree. The method used is reminiscent “inclusive predicates” in theory.

Cubical type theory provides a constructive justification to certain aspects of homotopy such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. paper describes semantics, expressed presheaf topos with suitable structure inspired by cubical sets, some higher inductive types. It also extends syntax for types spheres, torus, suspensions,truncations, pushouts. All these are justified...