roconnor

roconnor / PatriciaTrie.v

Created March 5, 2012 19:18

Implementation of Patrica Tries in Coq

	Require Import Bvector.
	Require Import Eqdep_dec.

	Set Implicit Arguments.
	Unset Strict Implicit.
	Unset Printing Implicit Defensive.

	Definition bCompare (x y : bool) : comparison :=
	match x, y with
	\| false, false => Eq

roconnor / ExtendedIncompletenessInQ0

Last active February 21, 2016 16:39

	// Define Computably Enumerable (aka recursively enumerable) predicates.
	CESet : (Nat -> o) -> o
	CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m)

	// Standard Model

	interpT : (Nat -> Nat) -> Term -> Nat
	interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m)

	interpF : (Nat -> Nat) -> Formula -> o

roconnor / MemoBinTree.v

Last active May 14, 2024 15:32

Memo Trie for funcitons over binary trees in Coq (no support for memoizing structually recursive functions though)

	(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *)
	Require Import Vectors.Vector.
	Import VectorNotations.

	Set Primitive Projections.
	Set Implicit Arguments.

	Inductive binTree : Set :=
	\| Leaf : binTree
	\| Branch : binTree -> binTree -> binTree.

roconnor / MemoOrdBinTree.v

Created May 14, 2018 18:31

Memoization for structurally recursive funcitons over binary trees in Coq (with poor performance).

	Require Import Arith.
	Require Import Omega.

	Set Primitive Projections.
	Set Implicit Arguments.

	Inductive binTree : Set :=
	\| Leaf : binTree
	\| Branch : binTree -> binTree -> binTree.

roconnor / NbE.v

Created May 19, 2024 20:56

Normalization by Evaluation of Simply Typed Lambda Calculus including Sum and Empty Types.

	(* This Normalization by Evaluation is based on mietek's <https://research.mietek.io/A201801.FullIPLNormalisation.html>.
	I've removed the continuations to give a purely tree-based implementation.
	This is operationally less efficent than using continuations, but it is hopefully easier to understand and potentially easier to verify correct.

	Checked with Coq 8.18.0
	*)

	Inductive Form :=
	\| Zero : Form
	\| One : Form