Firas Khalife
Projects

Systems I built end to end.

A distributed platform built to keep working when services fail, and a Python backend for the Rocq Prover (formerly Coq).

Featured · Nov 2023 – Oct 2024

A cloud-native grading platform

Microservices on Spring Cloud, events over RabbitMQ (with Kafka and WebClient versions built too), a database per service, Terraform on AWS. Built to keep working when services fail.
Java · Spring BootSpring CloudKeycloakRabbitMQKafkaPostgreSQLMongoDBRedisDockerTerraform · AWSReact · TypeScript
Run it: docker-compose repo ↗Follow one grade →
Final-year project · compilers · formal methodsJan – Jun 2024

Python extraction for the Rocq Prover

A new backend for the Rocq Prover (formerly Coq), the proof assistant, that turns its verified programs into Python.Rocq already extracts verified programs to OCaml, Haskell and Scheme; this adds Python.
Rocq Prover (formerly Coq)GallinaOCamlopamPython

Python extraction for the Rocq Prover

The Rocq Prover (formerly Coq) already extracts verified programs to OCaml, Haskell and Scheme; this adds Python. The hard part was a correspondence between Gallina’s grammar and Python’s, so pattern matching, inductive types and currying keep their meaning, in theory and not just on examples.

OCamlopamPython ASTpretty printer
khalifefiras29@gmail.comgithub.com/FirasKhalifelinkedin.com/in/firas-khalife