Tom de Jong
@de_Jong_Tom@mathstodon.xyz  ·  activity timestamp last week

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
Tom de Jong
@de_Jong_Tom@mathstodon.xyz  ·  activity timestamp last week

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

Kathy Reid
Kathy Reid boosted
ABC Feeds
@abcfeeds@rssfeed.media  ·  activity timestamp 2 weeks ago

Voice actors are already losing work to an AI disruption expected to reach everything
By Romy Stephens

The Productivity Commission says artificial intelligence could offer a $116 billion shot in the arm to Australia's economy. But for people like voice actor Colin Cassidy, that means a disruption to their daily work.

https://www.abc.net.au/news/2025-08-15/how-artificial-intelligence-could-threaten-jobs/105642364

#Technology#FederalGovernment#FederalParliament#ComputerScience#PerformingArts#RomyStephens
ABC Feeds
@abcfeeds@rssfeed.media  ·  activity timestamp 2 weeks ago

Voice actors are already losing work to an AI disruption expected to reach everything
By Romy Stephens

The Productivity Commission says artificial intelligence could offer a $116 billion shot in the arm to Australia's economy. But for people like voice actor Colin Cassidy, that means a disruption to their daily work.

https://www.abc.net.au/news/2025-08-15/how-artificial-intelligence-could-threaten-jobs/105642364

#Technology#FederalGovernment#FederalParliament#ComputerScience#PerformingArts#RomyStephens
MelHamnavoe
@MelvilleSpence@phpc.social replied  ·  activity timestamp 3 weeks ago
@derickr @ramsey @m1ke @maccath Ethics should be a compulsory part of any #softwareengineering #computerscience degree, is a hill I will happily die on. These weren’t kids off a bootcamp, these were senior BCS type engineers, who were happy to see their users jailed to save their blushes. There are no polite words to adequately describe these people.
Anyarchiste 😸 🏳️‍⚧️
@anyarchiste@is.nota.live  ·  activity timestamp 2 months ago

Okay dumb question:

We all know that the speed of your internet is as fast as the slowest component, right ?

So what is the point in having fiber to the home if the router goes only up to 2.5 GB/s on the outputs ?

Like, my super speed is wasted by the router at this point. Or am I getting something wrong ?

#Networking#ComputerScience
Terence Eden
@Edent@mastodon.social  ·  activity timestamp 2 months ago

🆕 blog! “It is 1939 and you want to use public-key cryptography”

Imagine, just for a moment, that a mathematical breakthrough had occurred on the eve of the second World War. Perhaps Turing or Rejewski or Driscoll realised that prime number theory held the key to unbreakable encryption. This blog post attempts to answer the question "could public-key …

👀 Read more: https://shkspr.mobi/blog/2025/07/it-is-1939-and-you-want-to-use-public-key-cryptography/
⸻
#ComputerScience #encryption
Terence Eden
@Edent@mastodon.social  ·  activity timestamp 2 months ago

🆕 blog! “It is 1939 and you want to use public-key cryptography”

Imagine, just for a moment, that a mathematical breakthrough had occurred on the eve of the second World War. Perhaps Turing or Rejewski or Driscoll realised that prime number theory held the key to unbreakable encryption. This blog post attempts to answer the question "could public-key …

👀 Read more: https://shkspr.mobi/blog/2025/07/it-is-1939-and-you-want-to-use-public-key-cryptography/
⸻
#ComputerScience #encryption
Nick Byrd, Ph.D.
@ByrdNick@nerdculture.de  ·  activity timestamp 3 months ago

How are concepts like 'reasoning' and 'inference' defined?

#Philosophy has definitions that go way back (e.g., in #epistemology and #PhilMind). Now #computerScience are realizing a need for definitions.

This #openAccess#CS review takes a crack at them: https://doi.org/10.48550/arXiv.2504.15900

"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"
"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"
"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"
Nick Byrd, Ph.D.
@ByrdNick@nerdculture.de  ·  activity timestamp 3 months ago

How are concepts like 'reasoning' and 'inference' defined?

#Philosophy has definitions that go way back (e.g., in #epistemology and #PhilMind). Now #computerScience are realizing a need for definitions.

This #openAccess#CS review takes a crack at them: https://doi.org/10.48550/arXiv.2504.15900

"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"
"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"
"...we formalize reasoning as a structured, multi-step process that dynamically decomposes complex problems, generates intermediate hypotheses, and iteratively refines solutions through logical and evidence-based transformations." "While inference I constitutes a single-step conditional probabilÎ𝑡=1 𝑇 ity computation 𝑃( 𝑦 |𝑥) = 𝑃( 𝑦 𝑡 |𝑥, 𝑦 <𝑡 ), reasoning R implements a meta-process coordinating multiple inference calls through explicit state management R(𝑥) = Φ 1 ◦ Φ 2 ◦ · · ·◦Φ 𝑛(𝑥). T"