ytakano

FROM httpd:2.4

ARG TITLE="OpenBSD"
ARG GIT=https://github.com/openbsd/src.git

#RUN sed -i 's/deb\.debian\.org/ftp\.jaist\.ac\.jp\/pub\/Linux/g' /etc/apt/sources.list

RUN apt-get -y update && \
    apt-get -y upgrade && \
    apt-get install -y tzdata

ytakano

モノイド

trait Monoid
where
    Self: PartialEq + std::fmt::Debug + Sized + Clone,
{
    const E: Self; // 単位元

    /// 乗算演算。self * rhs。 Self x Self -> Self

ytakano

corpus = ['abed', 'abet', 'abets', 'abut', 'acme',
          'acre', 'acres', 'actors', 'actress', 'airmen',
          'alert', 'alerted', 'ales', 'aligned', 'allergy',
          'alter', 'altered', 'amen', 'anew', 'angel',
          'angle', 'antler', 'apt', 'bade', 'baste',
          'bead', 'beast', 'beat', 'beats', 'beta',
          'betas', 'came', 'care', 'cares', 'casters',
          'castor', 'costar', 'dealing', 'gallery', 'glean',
          'largely', 'later', 'leading', 'learnt', 'leas',
          'mace', 'mane', 'marine', 'mean', 'name',

ytakano

Install F* on Ubuntu Linux

Install Opam

See below if you you use ubuntu 19.04

$ sudo apt install opam
$ opam init
$ eval `opam config env`

ytakano

#!/usr/bin/env sh

if [ $# -ne 1 ]; then
  echo "need epub file!" 1>&2
  echo "example:" 1>&2
  echo "    $ $0 ebook.epub" 1>&2
  exit 1
fi

FILE=`basename "$1" .epub`

ytakano

導出原理

p∨q, ¬p∨r
─────────
   q∨r

証明

ytakano

SF-TAP Flow Abstractorの更新

$ cd flow-abstractor
$ git pull origin master
$ make clean
$ cmake .
$ make

ytakano

!#/bin/sh

for i in `seq 0 15`
do
  PORT=`expr $i + 10000`
  echo socat TCP-LISTEN:$PORT,reuseaddr,fork UNIX-CLIENT:/tmp/sf-tap/tcp/http$i
  socat TCP-LISTEN:$PORT,reuseaddr,fork UNIX-CLIENT:/tmp/sf-tap/tcp/http$i
done

ytakano

#include <stdio.h>
#include <stdint.h>

#define TZCNTQ(DST, SRC)        \
    do {                        \
        asm (                   \
            "tzcntq %1, %0;"    \
            : "=r" (DST)        \
            : "r" (SRC)         \
            );                  \

ytakano

Refreed Papers

1. Sai Veerya Mahadevan, Yuuki Takano, and Atsuko Miyaji, “PRSafe: A Domain Specific Language Created with LLVM”, IPSJ, Electronic Preprint for Journal of Information Processing Vol.32, Feb. 2024
2. Yuuki Takano, "Deadlock- and Starvation-free Formally Verified Client Library for Robots", The 7th International Conference on System Reliability and Safety, ICSRS 2023, [PDF]
3. Atsuko Miyaji, Kaname Watanabe, Yuuki Takano, Kazuhisa Nakasho, Sho Nakamura, Yuntao Wang, and Hiroto Narimatsu, "Privacy-Preserving Distributed Medical Data Integration Security System for Accuracy Assessment of Cancer Screening: Development Study of Novel Data Integration System", JMIR Preprints, https://preprints.jmir.org/preprint/38922, Nov. 2022.
4. Sai Veerya Mahadevan, Yuuki Takano, Atsuko Miyaji, "PRSafe: Primitive Recursive Function based Domain Specific Lan