peterlefanulumsdaine / Oberwolfach Explorations
collaboration on work in progress
Projects that are alternatives of or similar to Oberwolfach Explorations
BusblasterKT-Link compatible buffer for the Bus Blaster v3
Stars: ✭ 6 (-40%)
Mutual labels: verilog
K18011801 series ULA reverse engineering
Stars: ✭ 16 (+60%)
Mutual labels: verilog
Lenet acceleratorA Lenet ASIC Accelerator targeting minimum number of cycles
Stars: ✭ 17 (+70%)
Mutual labels: verilog
AoocsThe OpenCores aoOCS SoC is a Wishbone compatible implementation of most of the Amiga Original Chip Set (OCS) and computer functionality. aoOCS is not related in any way with Minimig - it is a new and independent Amiga OCS implementation.
Stars: ✭ 23 (+130%)
Mutual labels: verilog
NaivecpuA CPU that implementing THCO-MIPS16 instruction set.
Stars: ✭ 5 (-50%)
Mutual labels: verilog
Sha512Verilog implementation of the SHA-512 hash function.
Stars: ✭ 10 (+0%)
Mutual labels: verilog
Tf530tf530
Stars: ✭ 22 (+120%)
Mutual labels: verilog
Novena Afe Hs FpgaHigh Speed Analog Front End FPGA Firmware for Novena PVT1
Stars: ✭ 8 (-20%)
Mutual labels: verilog
Fpga Srammystorm sram test
Stars: ✭ 16 (+60%)
Mutual labels: verilog
Upduino Ov7670 CameraDesign to connect Lattice Ultraplus FPGA to OV7670 Camera Module
Stars: ✭ 17 (+70%)
Mutual labels: verilog
OcpiSemi-private RTL development upstream of OpenCPI - this is *not* the OpenCPI repo!
Stars: ✭ 24 (+140%)
Mutual labels: verilog
Netlist GraphJava library for parsing and manipulating graph representations of gate-level Verilog netlists
Stars: ✭ 7 (-30%)
Mutual labels: verilog
Wb sdram ctrlSDRAM controller with multiple wishbone slave ports
Stars: ✭ 9 (-10%)
Mutual labels: verilog
Ie12A (very) minimal web browser for FPGAs implemented in Verilog
Stars: ✭ 6 (-40%)
Mutual labels: verilog
FftdemoA demonstration showing how several components can be compsed to build a simulated spectrogram
Stars: ✭ 23 (+130%)
Mutual labels: verilog
80211scramblerTools for working with the 802.11B scrambler when writing Packet-in-Packet exploits.
Stars: ✭ 10 (+0%)
Mutual labels: verilog
Amiga2000 GfxcardMNT VA2000, an Open Source Amiga 2/3/4000 Graphics Card (Zorro II/III), written in Verilog
Stars: ✭ 942 (+9320%)
Mutual labels: verilog
Explorations of (Synthetic) Homotopy Theory in Coq
These files contain some explorations/developments of homotopy theory inside intensional type theory, investigating the ideas discussed at the Oberwolfach mini-workshop in Feb/Mar 2011.
They are to be read with the propositional-equality-as-paths philosophy, as used in eg the univalent foundations of Voevodsky. The core concept is the inductive type usually thought of as propositional equality, considered instead as the space of paths (or morphisms, 1-cells…) between points of types. Thus types are considered as something like spaces, instead of just like sets; and so we can develop homotopy theory purely internally.
Currently contains files:
-
paths.v: Definition of path spaces, and basic workhorse functions for composition of paths, transport along paths, etc.
-
basic_weqs.v: Some basic homotopy-theoretic definitions — contractibility, weak equivalences, basic constructions with these. (Depends on paths.)
-
etacorrection.v: The propositional η-rule, and a couple of lemmas. (Depends on paths, basic_weqs.)
-
univalence.v: Voevodsky’s Univalence axiom, and its important equivalent form as an induction principle for weq’s. (Depends on paths, basic_weqs.)
-
pathspaces.v: Definition and constructions on the total path spaces of types. (Depends on paths, basic_weqs.)
-
fext_from_univalence.v: Deduction of functional extensionality from UA. (Depends on all the files above.)
-
higher-induction_experiments.v: investigating (approximations of) higher-dimensional inductive type definitions — the interval, the circle, and mapping cylinders. (Depends on paths.)
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at
[email protected].
