portfolio · résumé · est. 2007

Alex

MárquezPérezMuñízDíazPurasThaureauxFagúndoRivera

also @parcha · they/m // elle/él

GENERALIST COMPUTER SCIENTIST · SOFTWARE ENGINEER · SOFTWARE ARCHiTECT · FORMAL SEMANTICIST · MATHS & COMPUTER SCIENCE RESEARCHER

get in touchsee the workremote only

About

Senior engineer and scientist. Nearly two decades researching, designing, formalizing, prototyping, implementing, and maintaining solutions to complex problems.

A computer science generalist: from high-level software, APIs, and theory, down to low-level hardware architecture, compilers, and static analysis. Language-agnostic, with a specialty in type-driven development, object-oriented, and functional design. Fast and eager to learn new languages, techniques, frameworks, and paradigms.

Prefers collaborative environments, and puts a premium on being able to contribute to open source. Tech lead for teams of two to eight. Communicative to the point of “overly so”. Has taught and mentored in a variety of roles.

currently: open to senior software engineering roles — remote only.

Stack

languages

  • C
  • C++
  • Scala
  • Java
  • Python (2 & 3)
  • Rust
  • SQL (Postgres)
  • Bash
  • Gawk
  • Racket (& Redex)
  • LaTeX
  • Go
  • C#
  • Idris2

capabilities

  • type systems
  • metaprogramming & reflection
  • networking
  • multi-threading & shared memory
  • parallelization
  • inter-process communication
  • static analysis
  • compilation toolchains
  • ELF dynamic linkers
  • build systems (incl. Bazel)
  • GCC & LLVM optimizations
  • GDB
  • formal verification
  • operational semantics
  • Linux — kernel & userspace (incl. early)
  • x86 · ARM · AVR
  • Yocto & Buildroot
  • Git · Subversion · Perforce

natural languages

  • Englishtechnical
  • Spanishfluent — conversational & non-technical
  • Frenchreading & writing

security: TS Cleared

Work

  1. July 2024 – September 2025Remote

    Senior Software Engineer —Microsoft

    • Shipped core authentication — the Torus system that authenticates every user of all of Microsoft’s products and services.
    • Led resolution of security vulnerabilities across ControlPlane, Torus, RemoteAccess, and TorusPhoneApp.
    • Led design of an AI system that resolves routine security vulnerabilities and large dependency-upgrade rewrites across these products.
    • On-call for Service Authentication: 12-hour days for two weeks, five times a year.
    • Delivered technical talks and mentored engineers on the team.
  2. June 2021 – May 2023Atlanta, GA

    Software Engineer L5 —Google

    • Roboleaf: migrated Android’s custom Soong and Kati build system to Bazel.
    • Migrated the build of the Android platform’s binaries from Python to Bazel.
    • Built and maintained C and C++ object, static, and shared library build infrastructure, and its test infrastructure.
    • Broader “sheriff” for Bazel at Google: on-call triage of cross-cutting build issues.
    • Mentored junior engineers on C and C++ linking, programming languages, and build systems.
  3. November 2015 – March 2019Greenville, SC

    Cyber Engineer II — TS Cleared —Raytheon

    • Extended the runtime dynamic linker with new capabilities for a secure, soft real-time embedded Linux OS.
    • Built the build, deploy, provision, and maintenance tooling that monitored the MIL-STD-1553 bus for intrusions and anomalies, in kernel space and userspace; architecture focused on performance, fault tolerance, verifiability, and soft real-time behavior.
    • Wrote an scons + C++ sbuild module that obfuscated byte streams against static and dynamic analysis and reverse engineering.
    • Built PowerPC system emulation and test infrastructure.
    • Wrote firmware for an AVR ATmega32U4-based keyboard, including a proof of concept for malware propagation to a host.
    • Reverse engineered a heavily threaded x86-64 Linux network management server (SSL + CORBA RPC) to work around its licensing.
  4. July 2014 – April 2015Jupiter, FL

    Senior Software Engineer —DG Technology Group

    • Re-architected a proprietary real-time brokerage and trading platform: multiple C++ modules sharing a Postgres database.
    • Re-implemented the risk-management algorithms.
    • Python + SciPy analytics, with Pandas and Seaborn visualization.
  5. May 2012 – December 2013Boston, MA

    PhD Researcher —Northeastern University

    • Programming languages research: static analysis via abstract interpretation, verified compilers, software contracts, temporal logic, and automata.
    • Funded by a DARPA project on Android security.
  6. May 2011 – December 2012Atlanta, GA

    Graduate Researcher —Georgia Institute of Technology

    • DARPA UHPC project: informal and formal program analysis characterizing challenge problems and candidate architectures.
    • Built Cetus-UHPC: a Cetus PA/S2S derivative computing algebraic metrics of parallelizability and memory footprint for a restricted-C subset.
  7. April 2009 – May 2010Atlanta, GA

    Undergraduate Researcher —Georgia Institute of Technology

    • Co-developed AFABL: an agent-based simulation language for non-programmers, with runtime reinforcement learning adapting agent behavior in place of much static behavior programming.
  8. May 2007 – August 2007Boulder, CO

    Software Engineer Intern —Cisco Systems

    • Helped migrate the ASA codebase to Safer C; implemented and optimized the Safer C standard library.
    • Migrated developer policy; audited the Linux kernel components of the codebase.

Selected projects

C++23 · header-only · 2025 – present

ConcBuilder

Concurrent sequence library: the ConcTree and ConcRope, grow-only sequences with three synchronization modes — single-threaded mutable, reference-counted copy-on-write, and epoch-based RCU for lock-free reader snapshots. After Prokopec & Odersky (LCPC 2015).

Rust · 2026 – present

Agda MCP

Fully-featured MCP server for Agda daemons.

C++ · OpenMP · 2017 – present

Atlas

Charts and “decharts” information with π as an atlas: steganography, and lossless archival and expensive transmission — e.g. interplanetary communication.

Scala · Racket/Redex · May 2011 – August 2013

OOCFA2

First higher-order static analysis of Dalvik bytecode: 4,000 LOC of production-quality Scala, safe JVM reflection, and formal verification in Racket and Redex. Advisors: Pandé, Shivers, and Isbell. M.S. plus part of the Ph.D.

Java · program analysis · 2012

Cetus-UHPC

Cetus PA/S2S derivative: algebraic metrics of parallelizability and memory footprint for a restricted-C subset, for the DARPA UHPC project. Supervisors: Dr. Mark Richards, Mr. Dan Campbell.

C · C++ · ARM assembly · 2009

Multi-way branch prediction

An ISA-native, C-like switch statement and a novel ARM multi-way branch predictor; modified gem5, and modified clang/LLVM middle and back ends. With Dr. Milos Prvulović.

Education

  1. May 2012 – December 2013Boston, MA

    PhD candidate, Computer Science

    Northeastern University

    Programming languages. Withdrew with all coursework complete. Abstract interpretation, verified compilers (Hoare-style logics), software contracts, automata, temporal, spatial, and separation logics. Graduate teaching assistant for Dr. Matthias Felleisen’s Fundamentals I — introduction to systematic problem solving, open to all majors.

  2. Fall 2010 – Spring 2013Atlanta, GA

    M.S. in Computer Science — GPA 3.7

    Georgia Institute of Technology

    Thesis in programming languages. (The degree is in hardware architecture — the story on request.)

  3. Fall 2006 – Spring 2010Atlanta, GA

    B.S. in Computer Science, Honors Program — major GPA 3.8

    Georgia Institute of Technology

    Inaugural class of the honors program. Thesis in AI (machine learning & programming languages). Four curriculum specializations — intelligence, systems & architecture, devices, information internetworks (two make a degree). Member of Upsilon Pi Epsilon.

Contact

Open to senior software engineering roles — remote only. If you’re building something hard, I want to hear about it.