Discussion
Loading...

#Tag

  • About
  • Code of conduct
  • Privacy
  • Users
  • Instances
  • About Bonfire
theruran 馃捇 馃寪 :cereal_killer:
theruran 馃捇 馃寪 :cereal_killer: boosted
Tom de Jong
@de_Jong_Tom@mathstodon.xyz  路  activity timestamp 2 months ago

My paper "Continuous and algebraic domains in univalent foundations" with @MartinEscardo was accepted for publication by the Journal of Pure and Applied Algebra! 馃帀
https://martinescardo.github.io/papers/continuous-algebraic-domains-in-uf.pdf

This paper has its origin in my very first paper with Mart铆n (and my second paper overall) "Domain Theory in Constructive and Predicative Univalent Foundations" which appeared at Computer Science Logic (CSL) back in 2021.

Since then I wrote my PhD thesis on this topic (and worked on other things in type theory after) and the present paper is a revision of both the CLS'21 paper and my PhD thesis (which I completed in 2022).

Everything in the paper has been formalized and an HTML rendering of the Agda file that directly links the code to the paper can be found here: https://martinescardo.github.io/TypeTopology/DomainTheory.Continuous-and-algebraic-domains.html

#typetheory #agda #logic #math #computerscience

  • Copy link
  • Flag this post
  • Block
Tom de Jong
@de_Jong_Tom@mathstodon.xyz  路  activity timestamp 2 months ago

My paper "Continuous and algebraic domains in univalent foundations" with @MartinEscardo was accepted for publication by the Journal of Pure and Applied Algebra! 馃帀
https://martinescardo.github.io/papers/continuous-algebraic-domains-in-uf.pdf

This paper has its origin in my very first paper with Mart铆n (and my second paper overall) "Domain Theory in Constructive and Predicative Univalent Foundations" which appeared at Computer Science Logic (CSL) back in 2021.

Since then I wrote my PhD thesis on this topic (and worked on other things in type theory after) and the present paper is a revision of both the CLS'21 paper and my PhD thesis (which I completed in 2022).

Everything in the paper has been formalized and an HTML rendering of the Agda file that directly links the code to the paper can be found here: https://martinescardo.github.io/TypeTopology/DomainTheory.Continuous-and-algebraic-domains.html

#typetheory #agda #logic #math #computerscience

  • Copy link
  • Flag this post
  • Block
Log in

bonfire.cafe

A space for Bonfire maintainers and contributors to communicate

bonfire.cafe: About 路 Code of conduct 路 Privacy 路 Users 路 Instances
Bonfire social 路 1.0.0-rc.3.13 no JS en
Automatic federation enabled
  • Explore
  • About
  • Members
  • Code of Conduct
Home
Login