Skip to content

Instantly share code, notes, and snippets.

View gmalecha's full-sized avatar

Gregory Malecha gmalecha

63 followers · 12 following
View GitHub Profile
@gmalecha
gmalecha / meta.yml
Created May 5, 2020 20:13
debugging meta.yml
---
# configuration file for [coq-community templates](https://github.com/coq-community/templates)
fullname: cpp2v
shortname: cpp2v
organization: bedrocksystems
community: false
travis: false
synopsis: >-
Axiomatic semantics for C++ built on top of Clang and Iris including
@gmalecha
gmalecha / Imp.v
Created October 21, 2018 22:10
Denotational Imp
(* Simple semantics for the Imp programming language (with function calls)
* using interaction trees.
*
* Note: This file requires an version of the interaction tree library before the change in the encoding that
* occurred at 5cf173e0a901eb7f9b9f3f44f7bd52c6e3a3a86a.
*)
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import ExtLib.Structures.Monad.
Require Import ExtLib.Structures.Traversable.
@gmalecha
gmalecha / EffUnguarded.v
Created June 30, 2018 02:58
Demonstration of the importance of "tight" co-inductive definitions
Section Eff.
Variable eff : Type -> Type.
CoInductive Eff (T : Type) : Type :=
| ret (_ : T)
| interact {A : Type} (_ : eff A) (_ : A -> Eff T)
| delay (_ : Eff T).
Arguments ret {_} _.
Arguments interact {_ _} _.
Arguments delay {_} _.
@gmalecha
gmalecha / TypedAndUntyped.hs
Last active February 15, 2020 20:33
A single representation for both strongly and weakly typed terms
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
@gmalecha
gmalecha / ShapeIndexed.hs
Last active April 19, 2019 16:23
https://gmalecha.github.io/reflections/2017/pattern-matching-on-data-kinds
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
module ShapeIndexed where
import Data.Constraint
@gmalecha
gmalecha / ComputationalReflection.v
Created June 10, 2017 17:45
Talk from SF Types, Theorems, and Programming Languages Meetup
Require Import Coq.Lists.List.
Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.
(**
** Speeding up Proofs with Computational Reflection
** Gregory Malecha
** gmalecha.github.io
**
**)
@gmalecha
gmalecha / member_heq_eq.v
Last active February 22, 2017 07:04
Solution to member_heq_eq
Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.
Set Implicit Arguments.
Set Strict Implicit.
Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.
@gmalecha
gmalecha / member_heq_eq.v
Last active February 22, 2017 07:00
Shell of the proof of member_heq_eq.
Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.
Set Implicit Arguments.
Set Strict Implicit.
Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.
@gmalecha
gmalecha / QedHarmful.v
Created February 18, 2017 22:24
Code listing for gmalecha.github.io/reflections/2017/2017-02-18-Qed-Considered-Harmful/Qed-Considered-Harmful
Require Import Coq.Lists.List.
Set Implicit Arguments.
Set Strict Implicit.
Section hlist.
Context {T : Type}.
Variable F : T -> Type.
Inductive hlist : list T -> Type :=
| Hnil : hlist nil
@gmalecha
gmalecha / MtacCancel.v
Last active April 18, 2016 22:29
Trying out Mtac
(** An axiomatization of commutative monoids
**)
Parameter m : Type.
Parameter star : m -> m -> m.
Local Infix "*" := star.
Parameter one : m.
Axiom star_comm : forall a b : m, a * b = b * a.
Axiom star_assoc : forall a b c : m, (a * b) * c = a * (b * c).
Axiom one_star : forall a : m, one * a = a.