gelisam

-- | A proof of Löb's theorem in Haskell, in reply to [1].
-- 
-- Like Dan Piponi's post on the subject [2], we end up with a function which is
-- basically a spreadsheet evaluator.
-- 
-- Unlike Dan's post, our proof of Löb's theorem follows the Wikipedia
-- proof [3] very closely. Since the proof is using provability logic, we
-- need to encode the rules of provability logic inside Haskell.
-- In particular, we avoid the common mistake of representing the rule
-- 

bishboria

These links no longer work. Springer have pulled the free plug.

Graduate texts in mathematics

duplicates = multiple editions

A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen

A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen

wakita

SDK = xcrun -sdk macosx

all: compute.metallib compute

compute.metallib: Compute.metal
	# Metal intermediate representation (.air)
	$(SDK) metal -c -Wall -Wextra -std=osx-metal2.0 -o /tmp/Compute.air $^
	# Metal library (.metallib)
	$(SDK) metallib -o $@ /tmp/Compute.air