Theo Belaire tbelaire
tbelaire
/ dot_top_bot_mut.v
Created
April 21, 2016 20:18
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Set Implicit Arguments. | |
| Require Import LibLN. | |
| Require Import Coq.Program.Equality. | |
| (* ###################################################################### *) | |
| (* ###################################################################### *) | |
| (** * Definitions *) | |
| (* ###################################################################### *) |
tbelaire
/ Cargo.lock
Created
April 17, 2016 18:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [root] | |
| name = "hello" | |
| version = "0.1.0" | |
| dependencies = [ | |
| "core 0.1.0 (git+https://github.com/phil-opp/nightly-libcore.git)", | |
| "linux-std 0.1.0", | |
| "log 0.3.6 (registry+https://github.com/rust-lang/crates.io-index)", | |
| ] | |
| [[package]] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Compiling bindgen v0.16.0 (https://github.com/alexander255/rust-bindgen.git#88c54e09) | |
| Running `rustc /home/tbelaire/.multirust/toolchains/nightly/cargo/git/checkouts/rust-bindgen-32f69e0092dfc21d/master/build.rs --crate-name build_script_build --crate-type bin -g --out-dir /home/tbelaire/Code/rust.ko/target/debug/build/bindgen-317dda2c0a25a7ba --emit=dep-info,link -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps --cap-lints allow` | |
| Compiling rustc-serialize v0.3.19 | |
| Running `rustc /home/tbelaire/.multirust/toolchains/nightly/cargo/registry/src/github.com-88ac128001ac3a9a/rustc-serialize-0.3.19/src/lib.rs --crate-name rustc_serialize --crate-type lib -g -C metadata=3bc953984ed46e7f -C extra-filename=-3bc953984ed46e7f --out-dir /home/tbelaire/Code/rust.ko/target/debug/deps --emit=dep-info,link -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps -L dependency=/home/tbelaire/Code/rust.ko/target/debug/deps --cap-lints allo |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /* automatically generated by rust-bindgen */ | |
| pub type __int128_t = ::std::os::raw::c_void; | |
| pub type __uint128_t = ::std::os::raw::c_void; | |
| pub type __builtin_va_list = [__va_list_tag; 1usize]; | |
| #[repr(C)] | |
| #[derive(Copy)] | |
| pub struct Struct_ftrace_branch_data { | |
| pub func: *const ::std::os::raw::c_char, | |
| pub file: *const ::std::os::raw::c_char, |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top") -*- *) | |
| (* File reduced by coq-bug-finder from original input, then from Coq.Lists.List70 lines, Coq.Arith.Max lines to 97 lines, then from 197 lines to 115 lines, then from 129 lines to 115 lines *) | |
| Require Coq.Lists.List. | |
| Require Coq.Arith.Max. | |
| Require Coq.Arith.Peano_dec. | |
| Module Type ATOM. | |
| Parameter atom : Set. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top") -*- *) | |
| (* File reduced by coq-bug-finder from original input, then from Coq.Lists.List70 lines, Coq.Arith.Max lines to 97 lines, then from 197 lines to 115 lines, then from 129 lines to 115 lines *) | |
| (* coqc version 8.4pl6 (October 2015) compiled on Oct 12 2015 11:33:25 with OCaml 4.02.3 | |
| coqtop version 8.4pl6 (October 2015) *) | |
| Require Coq.Lists.List. | |
| Require Coq.Arith.Max. | |
| Module Type ATOM. | |
| Parameter atom : Set. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Inductive Nat := | |
| | Z : Nat | |
| | S : Nat -> Nat. | |
| Fixpoint plus (x : Nat) (y : Nat) : Nat := | |
| match x with | |
| | Z => y | |
| | S x' => S (plus x' y) | |
| end. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Inductive wf: envmode -> env typ -> env typ -> env val -> Prop := | |
| | wf_empty: forall m, wf m empty empty empty | |
| | wf_push: forall m e1 e2 s x T v, | |
| wf m e1 e2 s -> | |
| x # e1 -> | |
| x # s -> | |
| ty_trm ty_precise sub_general (get_ctx m e1 e2) (get_sigma m e1 e2) (trm_val v) T -> | |
| wf m (e1 & x ~ T) e2 (s & x ~ v). | |
| Definition wf_stack (G: ctx) (S: sigma) (s: stack): Prop := |
tbelaire
/ talk_ideas.txt
Last active
March 23, 2016 01:22
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Makefiles, here's how to use them. | |
| What's a Kernel Module: | |
| Adventures in getting the 360 controller light to stop spinning | |
| Racket Macros | |
| Racket Match: Never use first/rest again. | |
| Rust: Borrows | |
| Rust: Send + Sync gives you thread safety for free | |
| Rust in the Kernel. | |
| Coq: an introduction to induction | |
| Creating VTables in C for fun and profit (and dynamic dyspatch :P) |
tbelaire
/ CoqIntro.v
Created
March 14, 2016 19:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (**************************************************************) | |
| (** * Coq for POPL Folk *) | |
| (**************************************************************) | |
| (** A streamlined interactive tutorial on fundamentals of Coq, | |
| focusing on a minimal set of features needed for developing | |
| programming language metatheory. | |
| Mostly developed by Aaron Bohannon, with help from Benjamin | |
| Pierce, Dimitrios Vytiniotis, and Steve Zdancewic. |