You are not logged in |
Theorem Proving for All
- Speaker(s)
- Marcin Benke
- Affiliation
- MIMUW
- Date
- May 13, 2022, 12:15 p.m.
- Room
- room 5820
- Seminar
- Seminar Semantics, Logic, Verification and its Applications
Jedną z istotnych zalet czystych języków funkcyjnych, takich jak Haskell jest możliwość równościowego wnioskowania o programach. Jednakże do tej pory takie wnioskowanie miało charakter zewnętrzny względem programu: już to (najczęściej) ręcznie „na papierze”, już to mechanicznie w systemie takim jak Coq czy Isabelle.
W ramach seminarium, opowiem o pracy:
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton,
Theorem Proving for All - Equational Reasoning in Liquid Haskell (Haskell Symposium 2018),
która pokazuje, jak takie wnioskowanie może zostać wykonane wewnątrz Haskella i sprawdzone przy pomocy narzędzia Liquid Haskell.
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover.
During the seminar, I am going to talk about the paper:
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton,
Theorem Proving for All - Equational Reasoning in Liquid Haskell (Haskell Symposium 2018),
which shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell.
W ramach seminarium, opowiem o pracy:
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton,
Theorem Proving for All - Equational Reasoning in Liquid Haskell (Haskell Symposium 2018),
która pokazuje, jak takie wnioskowanie może zostać wykonane wewnątrz Haskella i sprawdzone przy pomocy narzędzia Liquid Haskell.
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover.
During the seminar, I am going to talk about the paper:
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton,
Theorem Proving for All - Equational Reasoning in Liquid Haskell (Haskell Symposium 2018),
which shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell.
