Clever Geek Handbook

Seminars of the JetBrains Research Language Tools Lab

The Language Tools Laboratory is a joint initiative of JetBrains and the Faculty of Mathematics and Mechanics of St. Petersburg State University .



Laboratory staff investigate:



  • formalization and verification of the semantics of programming languages ​​in the context of weak memory models;
  • logical and relational programming;
  • the theory of formal languages ​​and its applications;
  • metaprogramming, specialization and partial computing;
  • formal verification and application of SMT solvers.


The weekly workshops are attended by our staff and students as well as invited speakers. Recently, seminars have been recorded and can be viewed on Youtube . In this post we will share links and descriptions of past meetings, as well as tell you how not to miss the announcements of future events.







Past talks:



Persistent semantics of the ext4 filesystem and verification in it
: , . , — kernel panic. . , .



. Linux ext4 , C/++11. , GenMC , . , GenMC , vim nano.



:







Implementing Link Compression Heap in GraalVM Native Image
, . . . .



:







A Slightly Subcubic Algorithm for the Pathfinding Problem with Context-Free Constraints
, . , , , . , , , (n^{3-e}) ( ) ? , , ?



— - (CFL-reachability), . 30 . ? , — fine-grained complexity. , , "« »" CFL-reachability.



:







Construction of certified partial calculators
, , , . , — . , — . , . Coq, Coq .



:







Checking models in weak memory models
— . , , . GenMC, . GenMC ( , , RC11 IMM). (Promising, Weakestmo) , , GenMC. , (Promising, Weakestmo), «», - .



, GenMC. , GenMC , . Weakestmo, . GenMC, Weakestmo.



:







Higher order logic programming
λProlog. , λProlog HOAS , . , , . , .



:







Expressive Power of Higher-Order Types and Non-determinism
, , , , . , , , . , , , . , , , , .



:







Retooling Concurrency for OCaml
OCaml, . , ,



:







Representability of invariants of programs with algebraic data types
. . (LIA, LRA BV, ), ().



: , . , . , . -.



:







Development of compilers of domain-specific languages ​​for special processors
, - . compiler-in-the-loop, . , GCC LLVM, , , .



- . SMT, , . , .



:







Incorrect logic
, , . , ? , , , , . , , , — « » « »: , , , , , Relation Algebra.



:







Semantics of Recursive Types with Indexed Execution Steps
, . : ( ) ( ). Appel McAllester . , , . , , .



- () .



:







The next report on November 2 will be made by Anton Trunov on the topic “Indiscernible evidence: by definition, but without the K-axiom”. Join the Google Meet at 5:30 pm here .



Seminar announcement on November 2
, , , , . « ». , , .. , — , , , . , . , , , .



: Coq. SProp . Prop . SProp .



To receive announcements of our seminars:





More articles:


All Articles