# TypeSynth: synthetic methods in program verification

### Table of contents

 Beneficiary: Jonathan Sterling Award: Marie Skłodowska-Curie Actions Postdoctoral Fellowship Funder: European Commission, Horizon Europe Framework Programme (HORIZON) Host: Aarhus University, Center for Basic Research in Program Verification Years: 2022–2024 Amount: 214,934.4 EUR

Abstract. Software systems mediate a growing proportion of human activity, e.g. communication, transport, medicine, industrial and agricultural production, etc. As a result, it is urgent to understand and better control both the correctness and security properties of these increasingly complex software systems. The diversity of verification requirements speaks to a need for models of program execution that smoothly interpolate between many different levels of abstraction.

Models of program execution vary in expressiveness along the spectrum of possible programming languages and specification logics. At one extreme, dependent type theory is a language for mathematically-inspired functional programming that is sufficiently expressive to serve as its own specification logic. Dependent type theory has struggled, however, to incorporate several computational effects that are common in every-day programming languages, such as state and concurrency. Languages that support these features require very sophisticated specification logics due to the myriad details that must be surfaced in their semantic models.

In the context of dependent type theory, I have recently developed a new technique called Synthetic Tait Computability or STC that smoothly combines multiple levels of abstraction into a single language. Inspired by sophisticated mathematical techniques invented in topos theory and category theory for entirely different purposes, STC enables low-level details (even down to execution steps) to be manipulated in a simpler and more abstract way than ever before, making them easier to control mathematically. Perhaps more importantly, the STC method makes it possible to import ideas and techniques from other mathematical fields that are comparatively more developed than programming languages.

The goal of the TypeSynth project is to extend the successful STC approach to a wider class of programming models, in particular programming languages with effects.

## Bibliography

The following authors are represented in this bibliography: Carlo Angiuli, Lars Birkedal, Thierry Coquand, Daniel Gratzer, and Jonathan Sterling.

### Refereed Publications

 MSCS To appear What should a generic object be?J. SterlingMathematical Structures in Computer ScienceMarch 10, 2023BibTeX citation@unpublished{sterling:2023:generic, doi = {10.48550/ARXIV.2210.04202}, author = {Sterling, Jonathan}, title = {What should a generic object be?}, year = {2023}, note = {To appear, Mathematical Structures in Computer Science}, } 

### Unpublished Manuscripts

 Oct. 2022 Preprint Controlling unfolding in type theoryUnder reviewOctober 10, 2022BibTeX citation@unpublished{gratzer-sterling-angiuli-coquand-birkedal:2022, doi = {10.48550/ARXIV.2210.05420}, author = {Gratzer, Daniel and Sterling, Jonathan and Angiuli, Carlo and Coquand, Thierry and Birkedal, Lars}, title = {Controlling unfolding in type theory}, year = {2022}, note = {Unpublished manuscript} }  Oct. 2022 Preprint Denotational semantics of general store and polymorphismUnder reviewOctober 6, 2022BibTeX citation@unpublished{sterling-gratzer-birkedal:2022, author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars}, year = {2022}, month = jul, note = {Unpublished manuscript}, title = {Denotational semantics of general store and polymorphism}, }  Oct. 2022 Preprint Reflections on existential typesJ. SterlingOctober 1, 2022BibTeX citation@article{sterling:2022:existentials, doi = {10.48550/ARXIV.2210.00758}, author = {Sterling, Jonathan}, title = {Reflections on existential types}, publisher = {arXiv}, year = {2022}, note = {Unpublished manuscript}, }  Jun. 2022 Preprint Naïve logical relations in synthetic Tait computabilityJ. SterlingBibTeX citation@unpublished{sterling:2022:naive, author = {Sterling, Jonathan}, year = {2022}, month = jun, note = {Unpublished manuscript}, title = {Na\"{i}ve logical relations in synthetic {Tait} computability}, } 

### Workshop Presentations

 Dec. 2022 Invited Controlling unfolding in type theoryJ. SterlingWorkshop on Dependent Type Theory (to celebrate the Defense of Loïc Pujet)December 14, 2022

### Research Notes

 Oct. 2022 Notes Practical SemanticsJ. Sterlinglocal copyOctober 14, 2022

### Seminar Talks

 Nov. 2022 Invited Denotational semantics in impredicative guarded dependent type theoryJ. SterlingProgramming, Logic and Semantics, ITU CopenhagenNovember 8, 2022