Chiara Sarti

A Personal Website

  • She/Her
  • PhD Stu­dent
  • Cat The­o­rist
  • Office FS20 CL
  • Email CS2197

Hello!

I’m Chiara Sarti, a PhD stu­dent under the super­vi­sion of Prof. Jamie Vicary at the Com­puter Lab­o­ra­tory of the Uni­ver­sity of Cam­bridge. Within the depart­ment, I work as a mem­ber of the Cam­bridge Log­i­cal Struc­tures Hub (CLASH.)

My research inter­ests are focused around study­ing higher struc­tures, such as higher dimen­sional cat­e­gories, syn­thet­i­cally via their inter­nal lan­guages. These nor­mally take the form of depen­dent type the­o­ries, such as Homo­topy Type The­ory (HoTT) for groupoids, but I am also inter­ested in dia­gram­matic cal­culi.

A good exam­ple of a project I am proud to have worked on is homotopy.io. It is a proof assis­tant which allows one to do con­struc­tions in syn­thetic homo­topy the­ory entirely through a graph­i­cal cal­cu­lus for finitely-pre­sented semi­strict glob­u­lar n-cat­e­gories. If this does not make much sense to you, you can try out a tutorial I wrote for the tool.

I was not always a Com­puter Sci­en­tist. My aca­d­e­mic back­ground prior to PhD life was in pure Math­e­mat­ics: I did a B.Sc. in Math­e­mat­ics at King’s Col­lege Lon­don, to then join Part III of the Math­e­mat­i­cal Tri­pos at the Uni­ver­sity of Cam­bridge. I main­tain an active inter­est in foun­da­tions of Math­e­mat­ics.

Research Projects

Posetal Diagrams for Logically-Structured Semistrict Higher Categories

Preprint with Jamie Vicary, 2023.

We now have a wide range of proof assis­tants avail­able for com­po­si­tional rea­son­ing in monoidal or higher cat­e­gories which are free on some gen­er­at­ing sig­na­ture. How­ever, none of these allow us to rep­re­sent cat­e­gor­i­cal oper­a­tions such as prod­ucts, equal­iz­ers, and sim­i­lar log­i­cal tech­niques. Here show how the foun­da­tional math­e­mat­i­cal for­mal­ism of one such proof assis­tant can be gen­er­al­ized, replac­ing the con­ven­tional notion of string dia­gram as a geo­met­ri­cal entity liv­ing inside an n-cube with a pose­tal vari­ant that allows exotic branch­ing struc­ture. We show that these gen­er­al­ized dia­grams have richer behav­iour with respect to cat­e­gor­i­cal lim­its, and give an algo­rithm for com­put­ing lim­its in this set­ting, with a view towards future appli­ca­tion in proof assis­tants.

ABS
DOI
PDF

Zeta-regularized Lattice Field Theory with Lorentzian background metrics

Preprint with Tobias Hartung and Karl Jansen, 2022.

Lat­tice field the­ory is a very pow­er­ful tool to study Feyn­man’s path inte­gral non-per­tur­ba­tively. How­ever, it usu­ally requires Euclid­ean back­ground met­rics to be well-defined. On the other hand, a recently devel­oped reg­u­lar­iza­tion scheme based on Fourier inte­gral oper­a­tor zeta-func­tions can treat Feyn­man’s path inte­gral non-per­tu­ba­tively in Lorentz­ian back­ground met­rics. In this arti­cle, we for­mally zeta-reg­u­lar­ize lat­tice the­o­ries with Lorentz­ian back­grounds and iden­tify con­di­tions for the Fourier inte­gral oper­a­tor zeta-func­tion reg­u­lar­iza­tion to be applic­a­ble. Fur­ther­more, we show that the clas­si­cal limit of the zeta-reg­u­lar­ized the­ory is inde­pen­dent of the reg­u­lar­iza­tion. Finally, we con­sider the har­monic oscil­la­tor as an explicit exam­ple. We dis­cuss mul­ti­ple options for the reg­u­lar­iza­tion and ana­lyt­i­cally show that they all repro­duce the cor­rect ground state energy on the lat­tice and in the con­tin­uum limit. Addi­tion­ally, we solve the har­monic oscil­la­tor on the lat­tice in Minkowski back­ground numer­i­cally.

ABS
DOI
HTML
PDF

Homotopy.io

Proof assis­tant with Calin Tataru, Nick Hu, Lukas Heidemann and Jamie Vicary, 2022.

The homotopy.io proof assis­tant allows the con­struc­tion of com­pos­ite mor­phisms in a finitely-gen­er­ated semi­strict n-cat­e­gory, via a point-and-click user inter­face. Com­pos­ites are ren­dered as 2d and 3d geome­tries, and can be visu­alised in 4d as movies of 3d geome­tries. Beyond its fea­tures as a visual proof assis­tant, homotopy.io can also be used as an effec­tive tool to type­set string dia­grams: any 2d dia­gram con­structed in the proof assis­tant can be exported with ease into LaTeX/TikZ and SVG, with exper­i­men­tal sup­port for manim. The proof assis­tant is imple­mented in the Rust pro­gram­ming lan­guage, and com­piled to WebAssem­bly to run in the web browser.

CODE
NLAB
TUTORIAL
URL