leodemoura

import Lean

opaque g (n : Nat) : Nat

@[simp] def f (i n m : Nat) :=
  if i < n then
    f (i+1) n (g m)
  else
    m
termination_by n - i

AndrasKovacs

open import Data.Unit
open import Data.Product

infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_

data Obj : Set where
  ∙    : Obj
  base : Obj
  _*_  : Obj → Obj → Obj

henrytill

(** "Landin's Knot" - implements recursion by backpatching *)
let landins_knot f =
  let r = ref (fun x -> assert false) in
  let fixedpoint = f (fun x -> !r x) in
  r := fixedpoint;
  fixedpoint

let factorial =
  let g f x =
    if x = 0 then

Earnestly

C99 List of Undefined Behavior

From N1256: (See http://port70.net/~nsz/c/c99/n1256.html#J.2)

• A "shall" or "shall not" requirement that appears outside of a constraint is violated (clause 4).
• A nonempty source file does not end in a new-line character which is not immediately preceded by a backslash character or ends in a partial preprocessing token or comment (5.1.1.2).
• Token concatenation produces a character sequence matching the syntax of a universal character name (5.1.1.2).
• A program in a hosted environment does not define a function named main using one of the specified forms (5.1.2.2.1).
• A character not in the basic source character set is encountered in a source file, except in an identifier, a character constant, a string literal, a header name, a comment, or a preprocessing token that is never converted to a token (5.2.1).
• An identifier, comment, string literal, character constant, or header name contains an invalid multibyte character or does not

jcmckeown

(** 
Dybjer and Setzer provide a logical framework in which Induction-Recursion — 
mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A — 
becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }.  However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set.  The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.

In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products.  A more careful presentation might work on a fibration over functions,
 { AB : Type * Type & fst AB -> snd AB } -> Type
instead, but good luck with that.
*)

pix

all:
	@echo "gcc-4.4 && -fdelete-null-pointer-checks"
	@gcc-4.4 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fdelete-null-pointer-checks test-deref.c -o test-deref
	@./test-deref || true && 
	@echo "gcc-4.5 && -fdelete-null-pointer-checks"
	@gcc-4.5 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fdelete-null-pointer-checks test-deref.c -o test-deref
	@./test-deref || true
	@echo "gcc-4.4 && -fno-delete-null-pointer-checks"
	@gcc-4.4 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fno-delete-null-pointer-checks test-deref.c -o test-deref
	@./test-deref || true