ブラウザよりも高速アクセス！
14 関係: 型付きラムダ計算、リヨン高等師範学校、プレスバーガー算術、パリ第11大学、フランス国立工芸院、フランス国立情報学自動制御研究所、フリーソフトウェア、エコール・ポリテクニーク、カリー＝ハワード同型対応、クロスプラットフォーム、四色定理、無名関数、GNU Lesser General Public License、OCaml。
型付きラムダ計算
型付きラムダ計算（typed lambda calculus）とは、無名の関数の抽象表現にラムダ (\lambda) というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 \sigma\to\tau から成る。System T はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系ではペアノ算術において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して全称量化を施すことでポリモーフィズムを実現している。これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算は直観主義的型理論の基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。 一部の型付きラムダ計算には「派生型」の記法が導入されている。すなわち、A が B の派生型であるとき、型が A である全ての項は型が B でもある。派生型のある型付きラムダ計算は単に普通の型付きラムダ計算に結合型 (conjunctive type) と F^\leq (F-sub) を加えたものである。 以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 (Type: Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純な純粋型システムでもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF (Programming language for Computable Functions) は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。 型付きラムダ計算はプログラミング言語の新たな型システムの設計で重要な役割を演じている。型付け可能性は一般にプログラミングの好ましい属性を捉え、例えば、プログラムがメモリアクセス違反を起こさないようにするといったことが考えられる。 プログラミングにおいて、強い型付けのプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。Eiffelには "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、agent (p: PERSON): STRING do Result.
新しい！!: Coqと型付きラムダ計算 · 続きを見る »
リヨン高等師範学校
ルネ・デカルト学園（文学・社会科学） リヨン高等師範学校（仏：École Normale Supérieure de Lyon、略称 ENS-Lyon、エコール・ノルマル・シュペリウール・ドゥ・リヨン）は、フランスにおける高等教育機関グランゼコールの一つであり、グランゼコールや大学の教員・研究者を養成することを目的とする。.
新しい！!: Coqとリヨン高等師範学校 · 続きを見る »
プレスバーガー算術
プレスバーガー算術(Presburger arithmetic)とは加法を含む自然数に関する一階述語論理体系である。 モイジェシュ・プレスバーガーにより1929年に導入された。 プレスバーガー算術のシグネチャには加法と等号のみが含まれ乗法は省かれる。 公理には数学的帰納法の公理型を含む。 プレスバーガー算術は加法と乗法両方含むペアノ算術より弱い体系である。ペアノ算術とは異なりプレスバーガー算術は決定可能である。 これはプレスバーガー算術の言語で書かれた任意の閉論理式がプレスバーガー算術の公理で証明可能かどうかを判定するアルゴリズムが存在することを意味する。 この決定問題の計算複雑性は漸近的に二重指数関数であることがで示されている。.
新しい！!: Coqとプレスバーガー算術 · 続きを見る »
パリ第11大学
パリ第11大学（パリだい11だいがく、Université de Paris-Sud）は13あるパリ大学の１校。パリ南部の郊外オルセーに位置している。理学部、工学部、医学部、薬学部、法学部を有する。薬学部はシャトネ＝マラブリーに位置する。.
新しい！!: Coqとパリ第11大学 · 続きを見る »
フランス国立工芸院
フランス国立工芸院（フランスこくりつこうげいいん、Conservatoire national des arts et métiers: CNAM、コンセルヴァトワール・ナシオナル・デ・アール・エ・メティエ）は、フランス高等教育省が管轄する、科学と産業の振興のための教育研究機関。正式にはフランス国の「国立工芸保存院」と呼ぶ。フランスの"grand établissement"（特別高等教育機関）という区分に属する。 カトリック神父アンリ・グレゴワール (Henri Grégoire) により「工芸（Arts et Métiers：術と職、技能、技術）に関わるあらゆる機械、道具、設計図、記述物、書物を保存しよう」と提唱され、使われなくなっていたサン＝マルタン＝デ＝シャン小修道院 (l'abbaye St-Martin-des-Champs) の教会堂の建物を用いてフランス革命中の1794年10月10日に創設された。公式には1802年に開館した。パリ工芸博物館が付設されている。 当初は、発明品の収集が目的であったが、のちに教育の場となった。現在は、「社会人のキャリアアップ」として、「技術者資格取得」を目指す「継続的職業教育の場」として、「夜間講座」を提供するのが主な役割となっている。.
新しい！!: Coqとフランス国立工芸院 · 続きを見る »
フランス国立情報学自動制御研究所
INRIA（Institut National de Recherche en Informatique et en Automatique、 フランス国立情報学自動制御研究所）は、フランス政府研究省および、経済・財務省が共同管理するフランス国立研究所である。 1979年に、フランスの情報・制御分野の中心となる研究機関として設立された。 フランス国内に8ヶ所の研究施設（アキテーヌ、ブルターニュ、ロレーヌ、フランシュ＝コンテ、イル＝ド＝フランス、ノール＝パ・ド・カレー、コート・ダジュール、ラングドック＝ルシヨン、ローヌ＝アルプ）をもち、3000人以上の職員を抱える大規模な研究所である。.
新しい！!: Coqとフランス国立情報学自動制御研究所 · 続きを見る »
フリーソフトウェア
フリーソフトウェア (free software) とは、ソフトウェアのうち、フリーソフトウェア財団が提唱する自由ソフトウェアを指す。大半のフリーソフトウェアは無償（フリー）で配布されているが、定義に従えば、ここでいうフリーソフトウェアについて一次配布が無償である必要は必ずしもない。 フリーソフトウェア財団はフリーソフトウェアの定義を提示している。ソフトウェアライセンスについてはフリーソフトウェアライセンスを参照。 定義に照らして自由ではない、すなわち改造や再配布などに制限が掛かっていたり、ソースコードが開示されていない、無償で利用できるソフトウェアとは異なる概念であり、この場合はフリーウェアもしくは無料ソフトと呼ぶことが望ましいとフリーソフトウェア財団はしている。 逆に定義に従ったソフトウェアであれば、一次的な配布が有償であってもフリーソフトウェアと呼ぶことができる。ただし、前述したように配布が自由であるため、ほとんどのフリーソフトウェアは無償で配布されている。 また、現状強い影響力を持つ定義として、フリーソフトウェア財団の定義の他に、DebianフリーソフトウェアガイドラインとそれをベースにしたOpen Source Initiativeのオープンソースの定義がある。.
新しい！!: Coqとフリーソフトウェア · 続きを見る »
エコール・ポリテクニーク
ール・ポリテクニーク（École polytechnique、通称X）は、パリ市近郊パレゾーに位置するフランスの公立高等教育・研究機関。グランゼコールのひとつであり、4年の課程でIngénieur Polytechnicien の理工系学位を付与する。学生やディプロム授与者はポリテクニシャン（polytechnicien）と呼ばれる。学生の多くは、予備大学で2年間の数学と物理を学んだ後、または理学士（Bachelor of Science）を取得したのちに、本校を受験することとなる。 1794年のフランス革命中に、数学者ラザール・カルノーとガスパール・モンジュによって創設され、1804年にナポレオン・ボナパルトによって軍学校とされる。今日ではフランス国防省の配下にある。 ParisTechの設立メンバーとしてパリ近郊の各高等工科系の学校とグループを結んでいる。 "ポリテクニック"の語源となった学校であり、世界中にエコール・ポリテクニークをモデルとした学校・大学が存在する。理工系エリート（テクノクラート）養成の機関であり、同校からは3名のノーベル賞受賞者、1名のフィールズ賞受賞者、3名のフランス大統領、複数の企業CEOを輩出している。2015年Timesの世界大学ランキングによって、フランス国内において第一位と認定された。.
新しい！!: Coqとエコール・ポリテクニーク · 続きを見る »
カリー＝ハワード同型対応
リー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、Curry-Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。 At the very beginning, the Curry–Howard correspondence is.
新しい！!: Coqとカリー＝ハワード同型対応 · 続きを見る »
クロスプラットフォーム
プラットフォーム（cross-platform）とは、異なるプラットフォーム（例えばPC/AT互換機とMacintosh、あるいはWindows・macOS・FreeBSD・Linuxなどのように、仕様が全く異なる機械（ハードウェア）またはオペレーティングシステム）上で、同じ仕様のものを動かすことが出来るプログラム（ソフトウェア）のことを言う。同様の呼称にマルチプラットフォームがある。 また、家庭用ゲームにおいては「クロスプラットフォーム」と「マルチプラットフォーム」で意味が異なる場合がある。本項ではこのケースについても後述する。.
新しい！!: Coqとクロスプラットフォーム · 続きを見る »
四色定理
四色定理（よんしょくていり／ししょくていり、）とは、厳密ではないが日常的な直感で説明すると「平面上のいかなる地図も、隣接する領域が異なる色になるように塗り分けるには4色あれば十分だ」という定理である。.
無名関数
無名関数（anonymous functionあるいはnameless function）とは、名前付けされずに定義された関数のことである。無名関数を表現するための方法には様々なものがあるが、近年主流となっているのはラムダ式による記法である。無名関数を表現するリテラル式は、関数リテラル (function literal) とも呼ばれる。値がある場合は関数オブジェクトであるものが多い。.
GNU Lesser General Public License
GNU Lesser General Public License（以前は、GNU Library General Public Licenseだった）または GNU LGPL、単にLGPLは、フリーソフトウェア財団（Free Software Foundation、以下FSFと略称）が公開しているコピーレフト型のフリーソフトウェアライセンスである。八田真行による日本語訳ではGNU 劣等一般公衆利用許諾書と呼称している。.
新しい！!: CoqとGNU Lesser General Public License · 続きを見る »
OCaml
OCaml（ 、オーキャムル、オーキャメル）は、フランスの INRIA が開発したプログラミング言語MLの方言とその実装である。MLの各要素に加え、オブジェクト指向的要素の追加が特長である。かつては Objective Caml という名前で、その略として OCaml と広く呼ばれていたが、正式に OCaml に改名された。.
