Alvin Tang

I am currently a master's student at TU Wien with a focus on formal methods and logical calculi for computer science.

Recently as a research intern at the Institute of Science and Technology Austria (ISTA), I have been participating in the development of Iris-Lean with metaprogramming. Prior to that, I also worked with the Automation of Logic group at the Max Planck Institute for Informatics (MPI-INF) on first-order logic satisfiability checking.

Having completed my undergraduate degree at the Australian National University (ANU), my other projects also involved research in subtyping, corecursion and automated theorem proving.

Education

Oct 2026 – Present: Master's programme in Logic and Artificial Intelligence at the Technische Universität Wien (TU Wien)
Feb 2022 – Dec 2025: Bachelor of Advanced Computing (Research and Development) (Honours) at the Australian National University (ANU)
- First Class Honours, GPA: 6.844 out of 7, University Medal
- Check out the list of courses completed
Jun 2021: International Advanced Levels (IAL)
- A*A*A* in Mathematics, Further Mathematics and Physics

Experience

May 2026 – Sep 2026: Scientific Intern at the Institute of Science and Technology Austria (ISTA)
- Project with Prof Michael Sammler in the Programming Languages and Verification group
- Development of the Iris separation logic framework in Lean 4
- Implementing Iris Proof Mode tactics, features for the customised type class synthesiser and more using metaprogramming
Jan 2026 – Apr 2026: Research Intern at the Max Planck Institute for Informatics (MPI-INF)
- Project with Prof Christoph Weidenbach in the Automation of Logic group
- Further development of the Clause Learning from Simple Models (SCL) approach to first-order logic automated reasoning
- Implementing propositional abstraction features in SPASS-SCL-FOL
Jul 2021 – Aug 2021: Software Development Intern at Aura Labs
- Streamlining of internal DevOps pipeline with Jenkins, Docker, Webmin and nginx reverse proxy
- Automation of SSL certificate renewal with Ansible
- Creation of tools with Node.js and npm
- Revamping the company's website with Notion and Fruition

Publication

Alvin Tang and Dirk Pattinson. A Coinductive Representation of Computable Functions. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025), volume 342 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1–7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi: 10.4230/LIPIcs.CALCO.2025.7

Projects and Academic Writings

My projects at the ANU involve research in subtyping, corecursion and automated theorem proving.

Generalised Type Preprocessing for Integrated Subtyping

Supervisor: Dr Fabian Muehlboeck
Thesis available in the ANU Open Research Repository
Development of a framework for extending decidable subtyping systems in a modular and compositional manner through a normalisation scheme
Studies of framework instantiations for union types, intersection types and predicative higher-rank polymorphic types with reference to Scala 3's type system and alternatives

Computable Corecursive Functions: A Coalgebraic Approach to A Turing-Complete Model

Supervisor: Prof Dirk Pattinson
Paper published at CALCO 2025 (see below)
A functional model of computation operating on the coalgebraic data structure of finite/infinite binary sequences
Establishing the definition principle and proving representation theorems by building connections between general recursion and F-coalgebras

CEGAR-Tableaux for Non-Normal Modal Logics

Supervisor: Prof Rajeev Goré
Sponsored by the ANU Summer Research Scholarship program
Extending tableau calculi inspired by the Counterexample-Guided Abstraction Refinement technique for efficient automated theorem provers

Automated SELinux RBAC Policy Verification Using SMT

Supervisor: Dr Alwen Tiu
Co-authors: Divyam Pahuja, Klim Tsoutsman
Technical report available on arXiv
Formalising role-based access control policies in Security-Enhanced Linux using satisfiability modulo theories
Development of a parser and a translator in Rust and C

See my GitHub repository for other academic writings.