Por Paolo Pistone (Università di Bologna).
The interactions between logic and the theory of computation are plentiful and deep. On the one side, proof systems can be used to prove termination of certain classes of algorithms, or to establish complexity bounds. On the other side, higher-order programming languages, such as typed lambda-calculi, can be proved to capture the computational content of proofs.
However, there is one side of the theory of computation which was only marginally touched by this fruitful interaction, that is, randomized computation.
In this talk we introduce a family of logical systems based on a new class of counting quantifiers, assessing the extent to which one formula is true. We show that these logics provide ways to characterize some probabilistic complexity classes and to define a Curry-Howard correspondence for randomized computation.
Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604
