Search

We experimentally demonstrate all-optical flip-flop and inverter operations using two adjacent lasing wavelengths in a quantum-well microring laser, and that the state is switched between the flip-flop and inverter operations by changing the phase in the outer cavity composed of busline waveguides. We also propose multimodal rate equations for a microring laser taking into account clockwise and counter-clockwise light propagations. By comparing experimental results and simulated results based on the rate equations, the principle of the switching between the flip-flop and inverter operations is clarified.

To understand fungal contamination in the indoor environment of the disaster region, a field survey was performed to measure the number of fungal counts and identify isolates in the indoor air of prefabricated temporary housing, privately independent-housing, and rented apartments flooded by the East Japan Great Earthquake disaster tsunami. As a result, the period with the highest detected fungal count was from the rainy season to summer in independent-housing and rented apartments. Moreover, in the temporary housing, the fungal number increased further in winter as indicated by the maximum fungal-number throughout the measurement period. The detection frequency of Aspergillus species was relatively higher in the indoor air of temporary housing than in typical housing in the non-disaster area. Since Aspergillus is known as an allergenic genus, it requires careful attention to the health risk for residents. The extremely high level of fungal condensation in indoor air possibly occurred due to high relative humidity and loss of heat insulation in the building attics. It is suggested that this problem commonly happened in the cold region including the entire disaster region of the East Japan Great Earthquake.

We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by the first two authors but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The sized types allow us to parametrize the complexity by the size of inputs, and the usages allow us to achieve a kind of rely-guarantee reasoning on the timing each process communicates with its environment. We prove that our new type system soundly estimates the parallel complexity, and show through examples that it is often more precise than the previous type system of the first two authors.

LIPIcs, Volume 195, FSCD 2021, Complete Volume

Front Matter, Table of Contents, Preface, Conference Organization

A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_ℕ, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.’s recent work on reductions from program verification to HFL_ℕ validity checking.

We study the implicit computational complexity of constructor term rewriting systems where every function and constructor symbol is unary or nullary. Surprisingly, adding simple and natural constraints to rule formation yields classes of systems that accept exactly the four classes of languages in the Chomsky hierarchy.

In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project., Comment: In Proceedings HCVS 2021, arXiv:2109.03988