Search

• < Previous
• 1
• Next >

---

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence

Kazuyuki Asada ; Naoki Kobayashi ; Ryoma Sin'ya ; Takeshi Tsukada.

It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst&nbsp;[&hellip;]

---

A Logical Foundation for Environment Classifiers

Takeshi Tsukada ; Atsushi Igarashi.

Taha and Nielsen have developed a multi-stage calculus {\lambda}{\alpha} with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically&nbsp;[&hellip;]

---

A Probabilistic Higher-order Fixpoint Logic

Yo Mitani ; Naoki Kobayashi ; Takeshi Tsukada.

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL&nbsp;[&hellip;]

---