1 of 17
Download to read offline
Ad
Recommended
Why Kotlin?
Why Kotlin?Dev Ogiwara
?
Why we should use Kotlin instead of Java?
Let's see at Kotlin's modern features.笔贬笔という概念か?存在しない退屈な世界
笔贬笔という概念か?存在しない退屈な世界Yoshihiro Ohsuka
?
PHP BLT #1 ( http://phpblt.connpass.com/event/21929/ )で補欠になってしまったため発表できなかった発表資料。
AWS LambdaでPHPのスクリプトを動かす話。
贰颁厂クラスタの础尝叠配下に贰颁2上で动くコンテナと贵补谤驳补迟别で动くコンテナを建ててみた
贰颁厂クラスタの础尝叠配下に贰颁2上で动くコンテナと贵补谤驳补迟别で动くコンテナを建ててみたHiroaki Kaji
?
JAWS-UG コンテナ支部 入門編 #5 ようこそ Fargate
のLTで使用した資料ですFlowtype Introduction
Flowtype IntroductionTeppei Sato
?
歌舞伎座.tech#6「VirtualDOMとReact」でのLT発表資料
http://kbkz.connpass.com/event/11254/Linuxカーネルモジュール自作入門 kprobesでカーネル空間ブレークポイント
Linuxカーネルモジュール自作入門 kprobesでカーネル空間ブレークポイントuchan_nos
?
Introduction to kprobes, a Linux feature which allows you to set break points in a kernel address space. This presentation also introduces a book about kprobes and sysfs.Closure Compiler Updates for ES6
Closure Compiler Updates for ES6Teppei Sato
?
Meguro.es #2 でのLT発表資料
http://meguroes.connpass.com/event/25018/厂肠补濒补のコンパイル速度の话が闻きたいだろうし、するつもりだ
厂肠补濒补のコンパイル速度の话が闻きたいだろうし、するつもりだyoshiaki iwanaga
?
(12月5日 追記) 最後のおまけのページにあるDottyはまだコンパイラとしての機能も不足しており、ベンチマークの対象とするにはまだ不適切な感じでした。調査不足な内容を公開してしまい申し分けありませんでした(??ω?｀)
VOYAGE GROUPで行なわれた社内LT大会の発表資料です。
Scala Compilerのベンチマークをとってみました。
作業に使ったファイルはこちら => https://github.com/kiris/scalac-benchmarksアプリケーションエンジニアのためのクラウドインフラ再入門 (2/3)
アプリケーションエンジニアのためのクラウドインフラ再入門 (2/3)Takashi Sogabe
?
デブサミ2014 2月14日 14-E-3 「アプリケーションエンジニアのためのクラウドインフラ再入門」 (2/3) 講演資
吉田さん、曽我部、輿水さんの順で発表した資料の2つめ(OpenStack編)になります
輿水さんの資料: http://www.slideshare.net/samemoon/20140214-dev-summit20140214More Related Content
What's hot (12)
Flowtype Introduction
Flowtype IntroductionTeppei Sato
?
歌舞伎座.tech#6「VirtualDOMとReact」でのLT発表資料
http://kbkz.connpass.com/event/11254/Linuxカーネルモジュール自作入門 kprobesでカーネル空間ブレークポイント
Linuxカーネルモジュール自作入門 kprobesでカーネル空間ブレークポイントuchan_nos
?
Introduction to kprobes, a Linux feature which allows you to set break points in a kernel address space. This presentation also introduces a book about kprobes and sysfs.Closure Compiler Updates for ES6
Closure Compiler Updates for ES6Teppei Sato
?
Meguro.es #2 でのLT発表資料
http://meguroes.connpass.com/event/25018/Similar to Coq for Moblie Phone @ ML名古屋 (20)
厂肠补濒补のコンパイル速度の话が闻きたいだろうし、するつもりだ
厂肠补濒补のコンパイル速度の话が闻きたいだろうし、するつもりだyoshiaki iwanaga
?
(12月5日 追記) 最後のおまけのページにあるDottyはまだコンパイラとしての機能も不足しており、ベンチマークの対象とするにはまだ不適切な感じでした。調査不足な内容を公開してしまい申し分けありませんでした(??ω?｀)
VOYAGE GROUPで行なわれた社内LT大会の発表資料です。
Scala Compilerのベンチマークをとってみました。
作業に使ったファイルはこちら => https://github.com/kiris/scalac-benchmarksアプリケーションエンジニアのためのクラウドインフラ再入門 (2/3)
アプリケーションエンジニアのためのクラウドインフラ再入門 (2/3)Takashi Sogabe
?
デブサミ2014 2月14日 14-E-3 「アプリケーションエンジニアのためのクラウドインフラ再入門」 (2/3) 講演資
吉田さん、曽我部、輿水さんの順で発表した資料の2つめ(OpenStack編)になります
輿水さんの資料: http://www.slideshare.net/samemoon/20140214-dev-summit20140214OpenJDK コミュニティに参加してみよう #jjug
OpenJDK コミュニティに参加してみよう #jjugYuji Kubota
?
First step of contribution for OpenJDK in Japanese on JJUG CCC 2016 SpringXcode 5 で見つけた「どうでもいい」機能（厳選６つ） #cocoa_kansai, #yidev
Xcode 5 で見つけた「どうでもいい」機能（厳選６つ） #cocoa_kansai, #yidevTomohiro Kumagai
?
Xcode 5 で見つけた「どうでもいい」機能と題して、STUDIO SHIN (@studioshin) さま主催の「第55回 Cocoa 勉強会関西」と @takayama さま主催の「yidev東京第二回」のそれぞれで、Xcode 5 の再入門をテーマに話をさせて頂きました。
普段の開発の中ではあまり気に留める機会はないけれど、でも知っておくと楽しくなるかもしれない機能を紹介しています。
それぞれの会で少し内容を変えて発表したので、このスライドでは両方の内容を併せてひとつにまとめてあります。厂肠补濒补でのプログラム开発
厂肠补濒补でのプログラム开発Kota Mizushima
?
エンジニアサポート新年会2012 CROSS 次世代言語CROSS『Scala、Haskell、PythonでのWeb開発の紹介』
でのScala発表スライドです。RubyによるMac OS Xデスクトップアプリケーション開発入門
RubyによるMac OS Xデスクトップアプリケーション開発入門宏治 高尾
?
第44回オープンソースサロンで発表した『RubyによるMac OS Xデスクトップアプリケーション開発入門』の資料です。ここでは、RubyとMacでどのようなビジネスが考えられるかという観点から私の書籍を宣伝しています（笑Ad
More from Hiroki Mizuno (20)
Scala基礎勉強会: Featherweight Scalaの紹介および型付け規則の決定可能性について
Scala基礎勉強会: Featherweight Scalaの紹介および型付け規則の決定可能性についてHiroki Mizuno
?
The document introduces Featherweight Scala, a calculus for a subset of Scala. It defines the grammar and evaluation rules of Featherweight Scala, including terms, types, classes, methods, and fields. It also defines type checking rules and proves they are deterministic, ensuring a type can be uniquely determined for any program.骋补濒濒颈苍补による証明駆动开発の魅力
骋补濒濒颈苍补による証明駆动开発の魅力Hiroki Mizuno
?
The document discusses Coq and Gallina, the language used for formal proofs in Coq. It provides examples of proof goals, such as proving that reversing a list twice returns the original list, and that decoding and encoding with base64 returns the original string. It also lists several Coq-based projects, including CompCert for formally verified C code generation, and links to learning resources for Coq.颁辞辩による惭蝉驳笔补肠办の証明
颁辞辩による惭蝉驳笔补肠办の証明Hiroki Mizuno
?
ProofSummit2011 http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8 における発表「Frama-Cによるソースコード検証」 (mzp)
「Frama-Cによるソースコード検証」 (mzp)Hiroki Mizuno
?
This document discusses using the Frama-C framework to formally verify C and C++ code. It provides examples of using Frama-C to verify functions that find the minimum of integer values, including abs(), min(), and min3(). Specifications for these functions are written using the ACSL specification language. Frama-C is then used to prove that the implementations satisfy the specifications. The document also discusses how concepts from Frama-C like LE (less than or equal) can be mapped to similar concepts in languages like Coq that are used for formal verification.20110424 action scriptを使わないflash勉強会
20110424 action scriptを使わないflash勉強会Hiroki Mizuno
?
The document discusses ActionScript and the ActionScript Virtual Machine 2 (AVM2). It provides examples of ActionScript bytecode (ABC) and instructions. It compares AVM1 and AVM2, and explains how AVM2 improved performance through just-in-time compilation and garbage collection. Code examples demonstrate how to compile and disassemble ABC files using tools like Flex SDK and Tamarin.Coq to Rubyによる証明駆動開発@名古屋ruby会議02
Coq to Rubyによる証明駆動開発@名古屋ruby会議02Hiroki Mizuno
?
The document discusses using the Coq proof assistant to implement and verify algorithms in Ruby. It mentions encoding a Base64 algorithm in Coq and extracting it to OCaml, Haskell, Scheme and potentially Ruby. It provides examples of defining and proving properties of a factorial function in Coq and extracting implementations to other languages. It also discusses using Coq to model and verify other algorithms like sorting before generating Ruby implementations.証明駆动开発のたのしみ蔼名古屋谤别箩别肠迟会议
証明駆动开発のたのしみ蔼名古屋谤别箩别肠迟会议Hiroki Mizuno
?
The document discusses the benefits and challenges of proof-driven development using the Coq proof assistant. It describes how Coq can be used to formally prove properties about code during development. However, it also notes that Coq has limitations when dealing with large numbers, which can cause stack overflows. It also discusses using Coq to formally specify the MessagePack serialization format and prove properties about it.颁辞辩による証明駆动开発
颁辞辩による証明駆动开発Hiroki Mizuno
?
This document discusses the concepts of base64 encoding and decoding using various programming languages, including Ruby, Haskell, and OCaml. It presents test cases for ensuring that the decode function successfully reverses the encoding process. The document also mentions using QuickCheck for property testing in Haskell.NGK忘年会 2010 / CoqからRubyへ
NGK忘年会 2010 / CoqからRubyへHiroki Mizuno
?
The document discusses using the Coq proof assistant to develop verified programs and extracting them to other languages like Ruby. It mentions past Coq-related meetups and events held in Nagoya, Japan including a Coq party and Nagoya hackathon. Future plans include extracting a Coq-verified program to Ruby at an upcoming hackathon and a talk on Coq at the Nagoya Ruby conference in February 2011.SacalaZa #1
SacalaZa #1Hiroki Mizuno
?
1) The document discusses Scala and type inference using the Hindley-Milner type system. It provides examples of type inference in Scala and compares it to other languages like OCaml and Haskell.
2) Hindley-Milner type inference allows Scala to infer types for variables and functions without needing explicit type annotations in many cases. This is illustrated through examples of integer increment functions.
3) Type inference in Scala 3.0 aims to improve on the current approach and make types even more implicit, bringing it closer to languages like OCaml.CoqUn2010
CoqUn2010Hiroki Mizuno
?
- The document discusses garbage collection (GC) in Coq, including defining GC as a function that takes an initial and final memory state (m1 and m2) and exists an intermediate state (m) where the mark phase is applied to m1 and m and the sweep phase is applied from m to m2.
- Safety properties are defined for memory states including disjointness of free and closed elements, and lemmas are proved about the mark phase and sweep phase preserving safety and fully marking objects.
- Extraction from Coq to OCaml is briefly mentioned as a way to run GC implementations in OCaml.翱颁补尘濒础笔滨厂别补谤肠丑の绍介
翱颁补尘濒础笔滨厂别补谤肠丑の绍介Hiroki Mizuno
?
This document discusses Hoogle, an API search tool for Haskell, and proposes creating a similar tool called OCaml Hoogle for the OCaml programming language. It notes that OCaml Hoogle would search OCaml library documentation and provide type signatures of functions to help with code completion, as Hoogle does for Haskell. The document provides details on the implementation and links to related projects.Ad
Coq for Moblie Phone @ ML名古屋
- 1. Coq for MobiLe Phone みずぴー/mzp 1
- 2. 自己紹介 ? みずぴー / mzp ? 関数型言語が好きです ? 所属勉強会: なごやかScala, ProofCafe, スター トSML# 2
- 4. 尘锄辫の日常 その他 Twitter コーディング Tumblr
- 5. 尘锄辫の日常 その他 Twitter コーディング ←iPadでOK Tumblr
- 6. iPadでコーディングしたい ? そうだ、処理系を移植しよう ? ちょっとしたコーディングならiPadでも可能 ? ワンライナーの開発 ? 関数定義の確認 ? AppStoreの規約とかは後で考えよう..
- 7. mzpの主要言語 ? Ruby/Rails ? Scala ? SML# ? OCaml ? Coq
- 8. mzpの主要言語 ? Ruby/Rails ～移植する言語の条件～ 1.ARMで動作する ? Scala ? SML# ? OCaml ? Coq
- 9. mzpの主要言語 ? Ruby/Rails ～移植する言語の条件～ 1.ARMで動作する ? Scala 2.省メモリ ? SML# ? OCaml ? Coq
- 10. mzpの主要言語 ? Ruby/Rails ～移植する言語の条件～ 1.ARMで動作する ? Scala 2.省メモリ 3.まだやってない ? SML# ? OCaml ? Coq
- 11. Coqとは ? 関数型プログラミング言語 ? プログラムの性質を証明できる ? 様々な言語に変換可能: OCaml, Haskell, Scheme, Scala, Ruby 詳しくは: プログラミング Coq ～ 絶対にバグのないプログラムの書き方 ～ http://www.iij-ii.co.jp/lab/techdoc/coqt/ 11
- 12. Coqの特徴 ? マイナーだしAppleの審査をくぐり抜けそう ? チューリング完全じゃないしね ? OCaml製なので移植が楽(な気がした) 12
- 13. Coq for iOSの構成 Coq UIとか バイトコードインタプリタ iOS 13
- 14. バイトコードインタプリタの移植 ? C言語(とインラインアセンブラ)で書かれてる ? 「コンパイラのレジスタ割り当てとかクソ」 ? ARM向けのマクロを有効にして、Xcodeに 突っ込んだ 参考: OCaml for iOS http://code.google.com/p/ocaml-for-ios/wiki/ 14
- 15. バイトコード版Coq ? コンパイルオプションをいじって、ビルドした ? Cの関数はFFI経由で相互に呼び出せる let _ = Callback.register "eval" eval;; int ret = caml_callback(*caml_named_value("eval"), caml_copy_string(s)); 15
- 16. デモ 16
- 17. まとめ Coq for iPhoneによって開けた世界 ? どこでも証明できるようになった！！ ? OCaml製のプログラムなら何でも移植できる ? iOSのUI付きで ? Androidもたぶん大丈夫 17
Editor's Notes
- #2: \n
- #3: \n
- #4: さて、みなさまに近況報告があります。\n新しいiPadを買いました!!(ここでiPadをみせびらかす)\n
- #5: \n
- #6: \n
- #7: \n
- #8: \n
- #9: \n
- #10: \n
- #11: \n
- #12: \n
- #13: \n
- #14: \n
- #15: \n
- #16: \n
- #17: \n
- #18: \n
- #19: \n
- #20: \n
- #21: \n
- #22: \n