僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが，Brzozowski derivativeに基づいて正規表現エンジンを実装し，あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです． 折角practicalなプログラムを書いたのにCoqの中に閉じ込めておくのも勿体ないですし， OCamlで同様の正規表現エンジンを実装し，実行速度を見てみようと思います． *1 2018/12/16 Brzozowski derivativeの定義に誤りがあったため修正 Brzozowski derivativeとは？ ある正規表現が受理する言語の先頭から，文字を取り除いて得られる言語 *2を受理する正規表現をBrzozowski derivativeといい，以下のようにsystematicに求められます． ある正規表現が空文字列を

Unix system programming in OCamlXavier Leroy and Didier Rémy1stDecember , 2014 © 1991, 1992, 2003, 2004, 2005, 2006, 2008, 2009, 2010 Xavier Leroy and Didier Rémy, inria Rocquencourt. Rights reserved. Consult the license. Translation by Daniel C. Bünzli, Eric Cooper, Eliot Handelman, Priya Hattiangdi, Thad Meyer, Prashanth Mundkur, Richard Paradies, Till Varoquaux, Mark Wong-VanHaren Proofread by

Let’s discuss common ways to handle errors in OCaml, their shortcomings, and finally, how polymorphic variants may help. The discussion applies equally well to Reason ML. If you need an introduction to the topic, I recommend Real World OCaml chapter on Error Handling. As a reference point, we’ll take three hypothetical functions which can return errors and which we want to compose: Parser.parse, w

How OCaml type checker works -- or what polymorphism and garbage collection have in common There is more to Hindley-Milner type inference than the Algorithm W. In 1988, Didier Rémy was looking to speed up the type inference in Caml and discovered an elegant method of type generalization. Not only it is fast, avoiding scanning the type environment. It smoothly extends to catching of locally-declare

Introduction F* (pronounced F star) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or

This project allows to run OCaml programs on PIC microcontrollers.

2012年1月14日のジュンク堂書店池袋本店トークセッション「新春座談会 このコンピュータ書がすごい！ 2012年版〜2011年に出たコンピュータ書ならこれを読め！〜」にて本書が紹介された模様です．(2012/1/14記)補助資料正誤表演習システムガイド継続(EvalContML1)第一級継続(EvalContML4)参照(EvalRefML3)本演習システムを使っている講義京都大学 大学院情報学研究科 通信情報システム専攻 専門科目「プログラム意味論」(2013年度〜)京都大学 大学院情報学研究科 知能情報学専攻 専門科目「ソフトウェア基礎論」(2008年度〜2012年度)お茶の水女子大学 大学院人間文化創成科学研究科 理学専攻 情報科学コース「言語意味論」(2012年度)お茶の水女子大学 理学部 情報科学科「計算モデル論」(2012年度)Updated on 2022-05-25 21

Faster builds with omake, part 3: Caches In this (last) part of the series we have a closer look at how OMake uses caches, and what could be improved in this field. Remember that we saw in total double speed for large OMake projects, and that we also could reduce the time for incremental builds. In particular for the latter, the effect of caching is important. This text is part 3/3 of a series abo

Faster builds with omake, part 2: Linux The Linux version of OMake suffered from specific problems, and it is worth looking at these in detail. This text is part 2/3 of a series about the OMake improvements sponsored by LexiFi: Part 1: Overview Part 2: Linux (this page) Part 3: Caches (will be released on Tuesday, 6/23) The original publishing is on camlcity.org. While analyzing the performance ch

Faster builds with omake, part 1: Overview In the 2014 edition of the "which is the best build system for OCaml" debate the OMake utility was heavily criticized for being not scalable enough. Some quick tests showed that there was in deed a problem. At LexiFi, the size of the source tree obviously already exceeded the critical point, and LexiFi was interested in an improvement. LexiFi develops for