SatQMCert
A maple package to compute certificates of members in Archimedean Saturated Quadratic Modules. Code 
Software
BasicLemma
A maple package to compute Bezout-like polynomials for coprime and non-negative polynomials over compact semialgebraic sets. Code 
StrictlyPositiveCert
A maple package to compute certificates of strictly positive polynomial over Archimedean Quadratic Modules. Code 
haskell-grader
Haskell application to automatically evaluate student assignments for CS 357: Declarative Programming at UNM. Code
AXDInterpolator
This project implements an interpolation algorithm proposed in FoSSaCS 2021 using the Z3 API. The project allows the user to choose Z3, Mathsat, or SMTInterpol as interpolation engines. The tool returns a formula in SMTLIB2 format, which allows compatibility with model checkers and invariant generators using such a format. Code 
EUFInterpolator
Master thesis work implementing new interpolation algorithms for the theory of equality and uninterpreted functions (EUF), octagonal formulas, and its combination. Code 
Bosque Transpiler to \(F^{*}\)
Prototypical implementation of a transpiler embedding a subset of the Bosque semantics into the Proof-oriented programming language \(F^{*}\). Code