james@cpthuba.dev copied!
james@cpthuba.dev — bash
type 'help' for commands  ·  esc or 'exit' to close
cpthuba.dev

James Bingen

Gouda, Netherlands
scroll

Software engineer at ASML (Brion) via Itility. MSc Computer & Embedded Systems Engineering graduate from TU Delft. I'm interested in formal verification, computational lithography, digital systems design, low-level programming, and aviation & flight control systems.

formal verification theorem proving LEAN3 / LEAN4 Rocq complexity analysis digital systems C / C++ systems programming embedded systems ABI models low-level optimization
Jul 2026
Present
Software Engineer
ASML (Brion) via Itility · Netherlands
C++ Python computational lithography research
Sep 2025
Jun 2026
Intern
ASML · Veldhoven, Netherlands
Combining formal methods with ABI models at one of the world's leading semiconductor equipment companies.
formal methods ABI models C++
Feb 2021
Feb 2025
Teaching Assistant
Leiden University · Leiden, Netherlands
Taught across 6 courses over 4 years, covering algorithms, operating systems, programming paradigms, and software engineering.
Programming Techniques Operating Systems Software Engineering Concepts of Prog. Languages Programming Methodologies Algorithms & Datastructures
Sep 2023
Aug 2026
MSc Computer & Embedded Systems Engineering
Delft University of Technology
Thesis: Binary Interface Compatibility for Library Integration in C++
Built VeriABI, a formally verified ABI compatibility checker for C++ shared libraries. Its decision procedure is proved sound and complete in the Rocq proof assistant across three layers of the Itanium C++ ABI. On a 554 MB production library it completes in about four minutes against more than two hours for the closest comparable tool.
Rocq formal verification ABI compatibility C++ OCaml
Sep 2019
Aug 2023
BSc Computer Science
Leiden University
Thesis: Verification of Combinational and Sequential Circuits in LEAN3
Formally verified digital logic circuits including adders, multiplexers, and flip-flops in Lean 3. Proved both combinational and sequential circuit correctness within a proof assistant.
Lean 3 dependent types formal verification digital circuits
Chip8toGo
CHIP-8 emulator written in Go. Supports the full instruction set, ROM loading, and graphics display. Built for fun and as an exercise in emulator design.
Go emulator CHIP-8
Academic C Compiler (acc)
C compiler built with a group for the TU Delft Compiler Construction course. Written in Rust with an LLVM backend, optimization passes, CFG/AST visualization, and a web playground via WASM.
Rust LLVM compilers
Hyprland
Fixed a null pointer dereference crash in the layout manager triggered by ending a swipe gesture on a fullscreen tiled window. Merged and backported into v0.54.2.
C++ bug fix merged