Brigitte Pientka
where else to find them
linkedin:brigitte-pientka-8952131a
what they talk about
all 4 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 22 in the filters
who talks about the same things
- Ryan Kavanagh3 talks
- Deepak Garg18 talks
- Chuta Sano3 talks
- Jason Z. S. Hu6 talks
- Amal Ahmed25 talks
- Kenji Maillard11 talks
| title | conference | date |
|---|---|---|
| McTT: A Verified Kernel for a Proof Assistant | ICFP 2025 | 2025-10-12 |
A fully verified kernel for core Martin‑Löf type theory is implemented in Rocq, proving normalization, consistency and injectivity of constructors and proving… | ||
| Fusing Session-Typed Concurrent Programming into Functional Programming | ICFP 2025 | 2025-10-12 |
FuSes embeds a session-typed process calculus inside a pure functional language and ships a formal type system with operational semantics and a machine-checked… | ||
| McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory | WITS 2025 | 2025-01-25 |
A correct-by-construction Coq implementation of Martin-Löf type theory produces an end-to-end proof checker, with formalized cumulative universe hierarchy and… | ||
| A Type-Theoretic Framework for Certified Meta-programming | PEPM 2025 | 2025-01-21 |
Claims a two-level type theory where LF encodes object languages and Martin-Löf type theory runs meta-programs, so generated code is typed and manipulable… | ||
| Semantics-based program manipulation in the age of LLMs | PEPM 2025 | 2025-01-21 |
Panel records concrete experiments and workflows: VS Code + Copilot generates SystemVerilog that is iteratively checked and fixed against model checking… | ||
| Split Decisions: Explicit Contexts for Substructural Languages | CPP 2025 | 2025-01-20 |
Contexts as Resource Vectors frames contexts as lists whose entries carry tags from a resource algebra so consumption means changing tags rather than removing… | ||
| A Dependent Type Theory for Meta-programming with Intensional Analysis | POPL 2025 | 2025-01-19 |
Introduces DeLaM, a concrete dependent layered modal type theory that implements three layers (syntax, MLTT, meta) with quoting of open code, composition… | ||
| Message-Observing Sessions | OOPSLA 2024 | 2024-10-20 |
Most is a process language that adds message-observing session types — a restricted form of type-level computation — to binary session types so protocols on… | ||
| Mechanizing Session-Types using a Structural View: Enforcing Linearity without ... | OOPSLA 2023 | 2023-10-23 |
Claims a method that removes linear contexts by embedding linearity as local predicates, mechanizes a session-typed CP variant called structural classical… | ||
| CPP Business Meeting | CPP 2023 | 2023-01-16 |
Conference reports concrete numbers: 53 submissions, 25 accepted after a two‑month light double‑blind review with 33 PC members and about 20 external… | ||
| Moebius: Metaprogramming using Contextual Types | POPL 2022 | 2022-01-16 |
Moebius provides a formal metaprogramming core: a multi-level contextual modal lambda-calculus that generates System F–style polymorphic code, lets open code… | ||
| POPLMark reloaded: Mechanizing proofs by logical relations | ICFP 2020 | 2020-08-23 |
Proposes a benchmark that mechanizes logical-relation proofs by proving strong normalization via Kripke-style logical relations for simply-typed lambda… | ||
| nothing matches | ||