Stephan Boyer
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- LambdaConf2 editions2017–2018
on a stage with
never shared a talk
who talks about the same things
- Katherine Ye2 talks
- Gabriel Claramunt4 talks
- Harold Carr6 talks
- Philip Wadler14 talks
- Stephanie Weirich14 talks
- Nicolas Tabareau14 talks
| title | conference | date |
|---|---|---|
| Proving Theorems and Certifying Programs with Coq | LambdaConf 2018 | 2018-06-03 |
Concrete claims and code: Coq proofs are Gallina terms checked by the typechecker, Ltac scripts generate those terms, and proofs erase to runnable… | ||
| Unconference Coq | LambdaConf 2018 | 2018-06-03 |
Proofs are built interactively: start with a goal like n + 0 = n, use intro/induction/simple/reflexivity tactics to move variables, reduce and close base… | ||
| What are Dependent Types | LambdaConf 2017 | 2017-05-25 |
Claims that dependent types can encode arbitrary mathematical propositions and that a type checker enforces those properties statically. Demonstrations include… | ||
| Higher order Abstractions | LambdaConf 2017 | 2017-05-25 |
Defines and compares concrete Haskell type class implementations: Contravariant contramap :: (a -> b) -> f b -> f a with Predicate and function examples… | ||
| nothing matches | ||