A repository with correctness proves of the leftpad function written in HOL4, Isabelle, Agda, Idris, Coq and etc.
https://github.com/hwayne/lets-prove-leftpad
https://github.com/hwayne/lets-prove-leftpad
GitHub
GitHub - hwayne/lets-prove-leftpad: Proving leftpad correct two-dozen different ways
Proving leftpad correct two-dozen different ways. Contribute to hwayne/lets-prove-leftpad development by creating an account on GitHub.
Хороший блог на русском языке о системном программировании, радиоэлектроннике и микроконтроллерах.
https://eax.me
https://eax.me
Retro Recipes is a show focused on refurbrishing of retro computers and history of personal computing.
https://www.youtube.com/channel/UC6gARF3ICgaLfs3o2znuqXA
https://www.youtube.com/channel/UC6gARF3ICgaLfs3o2znuqXA
YouTube
Retro Recipes x Commodore
👾 Tech & TV nostalgia + your backstage portal to Commodore® from the CEO's desk 💁🏻♂️
Join The Fractics & the whole Commodore Crew! On select Saturdays we dive deep into retro tech, unbox history, and sail forward with a legacy we all share. Whether you’re…
Join The Fractics & the whole Commodore Crew! On select Saturdays we dive deep into retro tech, unbox history, and sail forward with a legacy we all share. Whether you’re…
GrafX2 is a modern pixel art editor highly inspired by the Amiga's version of Deluxe Paint. I like this program not only because of its functional strengths, but also because of the interface made with own retro-looking UI toolkit.
http://grafx2.chez.com/
http://grafx2.chez.com/
A Type 1 reference hypervisor for X86 supported by Intel and Linux Foundation. It targets the automotive and IOT applications.
https://projectacrn.org
https://projectacrn.org
Project ACRN™
Home - Project ACRN™
..Read more
Supplementary materials to the compilers course of the Michigan State University.
https://www.cse.msu.edu/~cse450/Lectures/
https://www.cse.msu.edu/~cse450/Lectures/
A denoscription of the way how BISON-generated LALR(1) parsers work internally, all the internal data tables are compared to the ones described in the well known Dragon Book.
https://www.cs.uic.edu/~spopuri/cparser.html
https://www.cs.uic.edu/~spopuri/cparser.html
A beautiful collection of extremely tiny compilers of simple programming languages.
https://github.com/marcpaq/b1fipl
https://github.com/marcpaq/b1fipl
GitHub
GitHub - marcpaq/b1fipl: A Bestiary of Single-File Implementations of Programming Languages
A Bestiary of Single-File Implementations of Programming Languages - marcpaq/b1fipl
An amazing list of articles written by Matt Might on various topics, from lambda calculus to compilers development, from tips for academic talks to cryptography.
http://matt.might.net/articles/
http://matt.might.net/articles/
A tribute to the original series of articles Let's Build a Compiler (Jack Crenshaw) written by Marcel Hendrix. The structure is the same, but the implementation language is Forth and the target is x86.
http://home.iae.nl/users/mhx/crenshaw/tiny.html
http://home.iae.nl/users/mhx/crenshaw/tiny.html
home.iae.nl
Let's Build a Compiler: Tiny Kiss in iForth
TINY and KISS implemented in iForth.
A nice talk at FOSDEM about writing a FORTH compiler for the classic Gameboy through reverse engineering of a working hello-world ROM.
https://fosdem.org/2019/schedule/event/retro_gbforth/
https://fosdem.org/2019/schedule/event/retro_gbforth/
archive.fosdem.org
FOSDEM 2019 - GBForth: Using Forth to understand the Game Boy
Perhaps you remember that I already wrote about the programming language Factor. Today I want to post a link to an unofficial tutorial for beginners, which makes clear the "taste of the language"
https://andreaferretti.github.io/factor-tutorial/
#forth #tutorial #programming
https://andreaferretti.github.io/factor-tutorial/
#forth #tutorial #programming
Отличная статья 2013 года о реализации клона Nintendo Entertainment System на базе отладочной платы Altera DE2-115 с FPGA.
https://m.habr.com/ru/post/185872/
https://m.habr.com/ru/post/185872/
Хабр
NES, реализация на FPGA
Добрый день! Я хочу рассказать о проекте игровой консоли Nintendo Entertainment System (NES) в реализации на FPGA. На постсоветском пространстве она известна как Dendy. Желающих посмотреть...
A nice explanation of the three projections of Futamura.
http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html?m=1
http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html?m=1
Sigfpe
The Three Projections of Doctor Futamura
Introduction The Three Projections of Futamura are a sequence of applications of a programming technique called 'partial evaluation' or 'sp...
Третьего марта в культурном центре ЗИЛ пройдет фестиваль фонда Эволюция Et Cetera с участием Михаила Гельфанда, Алексея Семихатова, Игоря Уточкина и лекторов фонда Эволюция.
Вход бесплатный. Требуется регистрация на мероприятие.
https://evolutionfund.ru/etc2019
Вход бесплатный. Требуется регистрация на мероприятие.
https://evolutionfund.ru/etc2019
evolutionfund.ru
Et cetera. Фестиваль фонда «Эволюция»
Zero Dereference pinned «Третьего марта в культурном центре ЗИЛ пройдет фестиваль фонда Эволюция Et Cetera с участием Михаила Гельфанда, Алексея Семихатова, Игоря Уточкина и лекторов фонда Эволюция. Вход бесплатный. Требуется регистрация на мероприятие. https://evolutionfund.ru/etc2019»
A source code of the perfect DOS extender with ability to run Win32 PE binaries! It has own replacements for the following Win32 DLLs: KERNEL32.DLL, ADVAPI32.DLL, USER32.DLL, GDI32.DLL and DDRAW.DLL.
https://github.com/Baron-von-Riedesel/HX
https://github.com/Baron-von-Riedesel/HX
GitHub
GitHub - Baron-von-Riedesel/HX: Home of the HX DOS Extender and its DPMI-host HDPMI.
Home of the HX DOS Extender and its DPMI-host HDPMI. - Baron-von-Riedesel/HX
A nice programming language looking like old C++ without all these modern features like type inference, lambdas and metaprogramming.
http://ec-lang.org/
http://ec-lang.org/
A very compact compiler compiler which supports a useful subset of POSIX yacc input language (written in C89).
https://c9x.me/yacc/
https://c9x.me/yacc/