Arrow Research search

Author name cluster

S. Hayashi

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
2 author rows

Possible papers

2

IROS Conference 2017 Conference Paper

Planning and control of stable ladder climbing motion for the four-limbed Robot "WAREC-1"

  • Xiao Sun 0005
  • Kenji Hashimoto
  • Tomotaka Teramachi
  • Takashi Matsuzawa
  • Shunsuke Kimura 0001
  • Nobuaki Sakai
  • S. Hayashi
  • Y. Yoshida

This paper describes an approach that enables the four-limbed robot “WAREC-1” to climb up and down vertical ladders stably. First, the four-limbed robot “WAREC-1” is introduced and dynamic stability conditions in multi-mass model for ladder climbing are proposed as the basis of judging whether a four-limbed robot is stable or not while climbing a vertical ladder. According to the proposed stability conditions, 3 different types of moment will directly affect the stability of the robot on a ladder: gravitational moment, inertial moment and reaction force moment. With the analysis of these 3 kinds of moments and the relationship among them, stability control methods are proposed to maintain stability of the robot on a ladder to the greatest degree and avoid their mutual interference. Combining with the stability conditions and stability control proposed, stable motion planning of climbing up and down a vertical ladder, a motion planning method proposed by the authors that allows independent path and time planning in trajectory planning is also applied to reinforce the efficiency of the stability control. Eventually, results from the simulation and physical robot verify the validity of the proposed control methods.

Details

I&C Journal 1994 Journal Article

Singleton, Union, and Intersection Types for Program Extraction

  • S. Hayashi

Two types theories, ATT and ATTT, are introduced. ATT is an impredicative type theory closely related to the polymorphic type theory of implicit typing of MacQueen et al. ((1986), Inform. and Control 71, 95-130). ATTT is another version of ATT that extends the Girard-Reynolds second order lambda calculus. ATT has notions of intersection, union, and singleton types. ATTT has a notion of refinement types as in the type system for ML by Freeman and Pfenning ((1991), in "ACM SIGPLAN ′91, " ACM Press), plus intersection and union of refinement types and singleton refinement types. We will show how singleton, union, and intersection types serve for development of programs without unnecessary codes via a variant of the Curry-Howard isomorphism. More exactly, they give a way to write types as specifications of programs without the unnecessary codes which are inevitable in the usual Curry-Howard isomorphism.

Details DOI
v2026.09.13