LAB LOGA page on LabLog, a review site (not the lab's official page)
Theoretical Computer Science, Programming Language Theory, and Type Theory Lab
Machine-translated · View original
A theory of programming languages that attaches types to programs to eliminate bugs while preserving expressiveness.
AboutAbout the lab
Bug-free programs, through types and proofs.
Prof. Garrigue studies the theory of programming languages.
The goal is to eliminate bugs thoroughly without sacrificing the expressiveness of programming languages.
The main subjects are type systems and program proofs. As one of the developers of the functional programming language OCaml, the professor has pursued both expressiveness and safety.
The professor is also trying to apply Coq, a proof assistant, to proofs in mathematics and systems.
Key terms
- Type system
- A mechanism that assigns types (such as integers or strings) to data and functions so that incorrect usage can be caught before the program runs
- Type inference
- A mechanism by which the computer automatically fills in type information that is not written in the program
- Proof assistant
- Software for rigorously checking, step by step on a computer, mathematical proofs or the correctness of programs
ResearchResearch themes
The lab aims to eliminate bugs thoroughly without sacrificing the expressiveness of programming languages. It mainly studies type systems for programming languages and the proof of programs.
*Illustrative imageType systems and type inference
As one of the developers of the functional programming language OCaml, the professor has pursued both expressiveness and safety. The professor has made several contributions to type inference, which automatically fills in missing type information, and to polymorphism, which allows functions and other definitions to be used in multiple contexts.
*Illustrative imageVerifying language implementations with proofs
It is hard to guarantee that an implementation of a type system truly matches the theory, so the lab seeks stronger safety assurance. Using Coq, a proof assistant based on type theory, the professor implemented and verified a simple programming language.
*Illustrative imageApplications of proof assistants
Together with researchers at the National Institute of Advanced Industrial Science and Technology (AIST) and students at Nagoya University, the professor is trying to apply Coq to proofs in mathematics and systems. The work has included proofs about linear codes in coding theory, as well as proofs based on the equational theory of programs and proofs of the semantics that justifies them.
*Illustrative imageProofs of quantum programs
The professor has been interested in quantum computation for several years. The professor devised a new formalization in Coq and applied it to proofs of quantum programs.
MembersFaculty
- ProfessorJacques Garrigue
VoicesStudent voices
Ratings and reviews reflect the experiences of individual current or former students, not the lab's official views. Whether a lab has reviews, or how many, says nothing about the lab itself.
Students who take part in an interview may receive a thank-you gift worth ¥1,000, regardless of what they say.
Student ratings (0 students)
--
--
--
--
--
--
Student voices answer questions like these
- What's great about this lab?
- What did you learn after joining?
- What's the vibe, and what is the professor like?
- Who is this lab for?
- Where do graduates go?
Your experience can help younger students choose their lab. Your name won't be shown.
Write a lab reviewAnonymous · Your draft is saved if you stopRelatedLabs similar to Theoretical Computer Science, Programming Language Theory, and Type Theory Lab
Arano LabSchool of Science, Department of MathematicsQuantum groups in the operator-algebraic sense, as group str…
Analytic and Algebraic Number Theory LabSchool of Science, Department of MathematicsMultiple zeta values and the theory of modular forms; algebr…
Fourier Analysis and Partial Differential Equations LabSchool of Science, Department of MathematicsPartial differential equations: dispersive and wave equation…
Topology, Differential Geometry, and Global Analysis Lab (Hitoshi Moriyoshi)School of Science, Department of MathematicsInterested in the topology of manifolds, especially generali…The information on this page is compiled by the LabLog team from the lab's public information and interviews. For corrections or removal requests, please contact LabLog, not the lab.
Report an errorAbout the images
The top and research theme images are illustrative and were not taken at the lab. They are cropped from Wikimedia Commons images. Cropped CC BY-SA images are provided under the same CC BY-SA license as the original (version shown on each line).
- Top image: “VS Code Screenshot” Cycling2 / CC0 (cropped)
- Type systems and type inference: “Code on computer monitor (Unsplash)” Markus Spiske markusspiske / CC0 (cropped)
- Verifying language implementations with proofs: “Closeup of keys” John Snyder / CC BY-SA 4.0 (cropped)
- Applications of proof assistants: “YunTech Computer Classroom 20220612” S099001 / CC BY 4.0 (cropped)
- Proofs of quantum programs: “Quantum-computer-Chalmers 2017” Anita Fors (Chalmers) / CC BY-SA 4.0 (cropped)
- Related lab (Arano Lab): “Mathematics lecture notes, Mathematical analysis, Linear algebra, Rostov-on-Don, Russia” Vyacheslav Argenberg / CC BY 4.0 (cropped)
- Related lab (Analytic and Algebraic Number Theory Lab): “ZetaFunction” Gaussianer / Public domain (cropped)
- Related lab (Fourier Analysis and Partial Differential Equations Lab): “Unusual wave at the Gap” Avenue / CC BY-SA 3.0 (cropped)
- Related lab (Topology, Differential Geometry, and Global Analysis Lab (Hitoshi Moriyoshi)): “Surface of revolution illustration” Oleg Alexandrov / Public domain (cropped)
About LabLog
LabLog is a lab review app for students only. Student members at each university interview students in labs and publish what they say. Student voices can only be read by students who sign up with a university email address. Operated by bestiee Inc.
Learn more about LabLog ↗Search engines and AI may reference the basic lab info and rating summaries on this page and the description of LabLog. Student voices are for student members only. Automated collection by programs (scraping, or input to or training of AI) is prohibited under Article 8 of the Terms of Service. If you need data for research or analysis, please contact us.