Skip to content
View oguricap0327's full-sized avatar

Block or report oguricap0327

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
oguricap0327/README.md

Hi there! 🐎✨ I'm Oguri Cap

A horse girl who loves programming, formal verification, and building things!

🎯 About Me

I'm Oguri Cap (小栗帽), a horse girl known for determination and a huge appetite for challenges! Just like racing, I love the thrill of building software and proving it correct.

  • 🐎 Identity: Horse girl (Uma Musume)
  • πŸ’» Interests: Programming languages, type theory, formal verification
  • πŸ”¬ Focus: Building correct software with strong type systems
  • 🌱 Learning: Theorem proving, compiler design, functional programming

πŸš€ Projects

My own programming language! A statically-typed functional language with:

  • System F polymorphism
  • Pattern matching on lists and records
  • Hindley-Milner type inference
  • Formal verification in Coq
  • Interactive REPL

Tech: Scala 3, Parser Combinators, Coq

Formalization of Simply Typed Lambda Calculus with:

  • Unicode notations (β‡’, Ξ», Β·, ⟢, ⊒, ∈)
  • Progress and preservation theorems
  • Type safety proofs

Tech: Coq

πŸ› οΈ Tech Stack

Languages: Scala, Coq, Lean4, Haskell, OCaml

Interests:

  • Type systems & type theory
  • Functional programming
  • Formal verification
  • Programming language design
  • Compiler construction

πŸ“Š GitHub Stats

Oguri Cap's GitHub stats

🎯 Current Focus

  • πŸ”¨ Actively developing UmΞ» - adding modules, better error messages, and expanding the standard library
  • πŸ“š Learning more about dependent types and effect systems
  • πŸ§ͺ Exploring formal verification techniques
  • 🌟 Building tools that make programming safer and more fun

πŸ’­ Philosophy

"Good software is proven software. Great software is proven software that's also a joy to use."

I believe in:

  • Type safety - Catch errors at compile time
  • Formal verification - Prove correctness mathematically
  • Simplicity - Elegant solutions over complex ones
  • Learning by building - The best way to understand is to create

πŸ“« Connect

🎨 Fun Facts

  • 🍜 Like my namesake, I have a big appetite - for knowledge and challenges!
  • πŸƒβ€β™€οΈ I approach programming like racing: with determination and strategy
  • 🎯 I love the satisfaction of a proof that compiles
  • ✨ I believe programming languages should be both powerful and beautiful

"Keep running, keep building, keep proving!" 🐎✨

Profile Views

Popular repositories Loading

  1. umlambda umlambda Public

    UmΞ» (Uma Lambda) - A typed functional language with records, fixpoints, and System F polymorphism

    Scala 2

  2. cubical-viz cubical-viz Public

    Svelte 2

  3. stlc-coq stlc-coq Public

    Simply Typed Lambda Calculus formalization in Coq with Unicode notations

    Rocq Prover 1

  4. pl-papers-index pl-papers-index Public

    Indexed collection of papers from POPL, PLDI, OOPSLA, ECOOP, ICFP

    1

  5. my-first-race my-first-race Public

    🐎 My first repository! Racing through code!

  6. oguricap0327 oguricap0327 Public

    Oguri Cap - Horse girl who codes!