Skip to content

Instantly share code, notes, and snippets.

View y-taka-23's full-sized avatar

Cheshire Cat y-taka-23

83 followers · 31 following
View GitHub Profile
@y-taka-23
y-taka-23 / rnpcalc.cob
Last active August 29, 2015 14:04
COBOL による逆ポーランド電卓
IDENTIFICATION DIVISION.
PROGRAM-ID. RNPCALC.
DATA DIVISION.
WORKING-STORAGE SECTION.
01 STACK-POS PIC 9(2) VALUE 1.
01 STACK.
03 STACK-DATA PIC 9(4) OCCURS 10 VALUE 0.
01 EXPR PIC X(20).
01 EXPR-POS PIC 9(2).
@y-taka-23
y-taka-23 / fibonacci.cob
Created July 27, 2014 04:43
COBOL による Fibonacci 数の計算
IDENTIFICATION DIVISION.
PROGRAM-ID. FIBONACCI.
DATA DIVISION.
WORKING-STORAGE SECTION.
01 ARGUMENT PIC 9(2).
01 RETURN-VALUE PIC 9(25).
01 RESULT PIC Z(25).
01 DP-TABLE.
03 VALS PIC 9(25) OCCURS 99.
@y-taka-23
y-taka-23 / death_march_05.cob
Last active August 29, 2015 14:05
CodeIQ「第 5 回デスマコロシアム」の固定形式 COBOL 85 による実装
IDENTIFICATION DIVISION.
PROGRAM-ID. DEATH-MARCH-05.
DATA DIVISION.
WORKING-STORAGE SECTION.
77 FB-STR PIC X(153).
77 CNT PIC 9(2) VALUE 1.
77 QUOT PIC 9(2).
77 REM-3 PIC 9(1).
77 REM-5 PIC 9(1).
@y-taka-23
y-taka-23 / promela_sharing.pml
Created December 14, 2014 14:58
An Invalid (Deadlocked) Model of Resource Sharing Problem
/*
* Resource Sharing Problem (Example for Deadlock)
*/
mtype = { LOCK, UNLOCK };
proctype Client(chan to_res1, to_res2) {
if
:: to_res1 ! LOCK(_pid);
to_res2 ! LOCK(_pid);
@y-taka-23
y-taka-23 / coq_uniq.v
Created September 12, 2015 06:31
An Implementation of the uniq Command Certified by Coq
Parameter A : Type.
Parameter beq_A : A -> A -> bool.
Section Uniq.
Require Import Arith List.
Hypothesis beq_A_true : forall x y : A,
beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,
@y-taka-23
y-taka-23 / coq_kleisli.v
Last active December 10, 2015 01:28
Kleisli Construction of Monads (Equivalency of Category Theory Style and Haskell Style)
(******************************************************)
(** //// Kliesli Construction of Monads //// *)
(******************************************************)
Require Import Logic.FunctionalExtensionality.
(*////////////////////////////////////////////////////*)
(** Preliminaries *)
(*////////////////////////////////////////////////////*)
@y-taka-23
y-taka-23 / coq_mlattice.v
Created December 22, 2012 17:10
An Example of Modular Lattices (The Lattice of Normal Subgroups of a Group)
(******************************************************)
(** //// Modular Lattices //// *)
(******************************************************)
Section ModularLattice.
Require Import Relation_Definitions Setoid Morphisms.
(*////////////////////////////////////////////////////*)
@y-taka-23
y-taka-23 / coq_topology.v
Created January 6, 2013 12:24
A Proof of the Elementary Property of Connected Spaces
(******************************************************)
(** //// Topology Spaces //// *)
(******************************************************)
Section Topology.
(*////////////////////////////////////////////////////*)
(** Axioms *)
(*////////////////////////////////////////////////////*)
@y-taka-23
y-taka-23 / coq_qsort.v
Last active December 11, 2015 01:49
Validation of the Quick Sort
(******************************************************)
(** //// Validation of the Quick Sort //// *)
(******************************************************)
Section QuickSort.
Require Import Arith List.
Require Import Recdef.
Require Import Sorting.Sorted Sorting.Permutation.
@y-taka-23
y-taka-23 / coq_stackcomp.v
Created July 27, 2013 07:34
Validation of the Compiler for the Stack Machine (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Imp.html.html)
(*******************************************************)
(** //// Validation of the Stack Machine Compiler //// *)
(*******************************************************)
Require Import List.
(* Definition : Identifiers *)
Inductive id : Type :=
| Id : nat -> id.