Seminar tomorrow

[Jan Kofron]

Dear all,

Let me invite you to another seminar in this semester that will take 
place on Tuesday, Oct 8, at 14:00 in S9 [1]. There will be *two* short 
talks, the first one given by Maya Mückenschnabel (Algebraic Effect 
Handlers with Bidirectional Type-Checking), and the other one by Jan 
Liam Verter (Don’t Call Us, We’ll Call You). Both are conference talk 
rehearsals.

[1] https://d3s.mff.cuni.cz/seminar/

Thanks, best regards!
Jan

====

Algebraic Effect Handlers with Bidirectional Type-Checking

In the development of type systems there are multiple paths for 
achieving more expressiveness. On the one hand, algebraic effect 
handlers allow us to reason about program's side effects. On the other 
hand, dependent types make it possible to more precisely reason about 
program states and data and to prove general mathematical statements. 
Our work is concerned with the development of a practical Lisp-based 
programming language that combines dependent types with effect handlers. 
More specifically we focus on describing the type system that has the 
two following features. First it combines the algebraic effect system 
with the bidirectional type-checking algorithm in order to support 
effects in dependent types. Second, it introduces further type inference 
rules for greater flexibility.

====


Don’t Call Us, We’ll Call You (Towards Mixed-Initiative Interactive 
Proof Assistants for Programming Language Theory)

There are two kinds of systems that programming language researchers use 
for their work. Semantics engineering tools let them interactively 
explore their definitions, while proof assistants can be used to check 
the proofs of their properties. The disconnect between the two kinds of 
systems leads to errors in accepted publications and also limits the 
modes of interaction available when writing proofs. When constructing a 
proof, one typically states the property and then develops the proof 
manually until an automatic strategy can fill the remaining gaps. We 
believe that an integrated and more interactive tool that leverages the 
typical structure of programming language could do better. In the early 
work presented in this paper, we focus on the problem of interacting 
with a proof assistant. Rather than starting with manual proof 
construction and then completing the last steps automatically, we 
propose a way of working where the tool starts with an automatic proof 
search and then breaks when it requires feedback from the user. Our 
early experience suggests that this way of working can make proof 
construction easier.



-- 
Jan Kofron, Ph.D.
Associate Professor
Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University
Malostranske namesti 25
118 00 Praha 1, Czech Republic
Phone: +420 95155 4285
http://d3s.mff.cuni.cz/~kofron
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 236 bytes
Desc: OpenPGP digital signature
URL: <http://d3s.mff.cuni.cz/pipermail/seminar/attachments/20241007/58bc16bd/attachment.sig>