[New Blog Post] Implementing E Unification using SMT https://www.philipzucker.com/smt_unify/ #logic #automatedreasoning #smt
Debby ⁂📎🐧:disability_flag:
boosted
Happy #Halloween
Happy #Halloween
Michelle Hughes
and 4 others
boosted
Djoerd Hiemstra 🍉
and 1 other
boosted
The 2026 Netherlands Winter School on Logic and Verification will take place Tuesday 20-Friday 23 January, 2026 at University of Twente. The school provides classes for PhD/graduate students in theoretical computer science, with a focus on software verification, logic, and type theory. Strong master students, as well as researchers and practitioners, are equally welcome. Participants are expected to have a background in theoretical computer science, mathematics or a related discipline at a master’s level, and have basic familiarity with (functional) programming, semantics, and logic.
cyclic-structures.gitlab.io/school2026/
Please consider registering! If you're a PhD student registered with the IPA school it will (very likely) be possible to get the costs reimbursed, but anyone with their own funding is welcome too.
#Logic #Verification #TypeTheory #CategoryTheory #Coinduction #SessionTypes #Concurrency #Rocq #Agda #Iris
The 2026 Netherlands Winter School on Logic and Verification will take place Tuesday 20-Friday 23 January, 2026 at University of Twente. The school provides classes for PhD/graduate students in theoretical computer science, with a focus on software verification, logic, and type theory. Strong master students, as well as researchers and practitioners, are equally welcome. Participants are expected to have a background in theoretical computer science, mathematics or a related discipline at a master’s level, and have basic familiarity with (functional) programming, semantics, and logic.
cyclic-structures.gitlab.io/school2026/
Please consider registering! If you're a PhD student registered with the IPA school it will (very likely) be possible to get the costs reimbursed, but anyone with their own funding is welcome too.
#Logic #Verification #TypeTheory #CategoryTheory #Coinduction #SessionTypes #Concurrency #Rocq #Agda #Iris
Kathy Reid
boosted
The official ads are now out for the #ANU #Logic Summer School, to be held in #Canberra , Australia from 1-12 December. https://comp.anu.edu.au/lss/
Paraphrasing a bit to fit in a toot:
OVERVIEW
The ANU Logic Summer School is an annual event that offers a two week long programme of lectures on modern logic, the foundational discipline of the information sciences. Topics include not only the science of reasoning but also computability theory, type theory and other tools for understanding processes, declarative programming, automatic proof generation, program verification and much more. The school is primarily geared at late undergraduate and masters students, but is open to all, including postgraduate and PhD students, postdocs, and participants from industry.
PROGRAMME
Week 1:
John Slaney (ANU): Foundations of Metalogic
Michael Norrish (ANU): Computability and Incompleteness
Peter Baumgartner (CSIRO): Overview of Automated Reasoning
Liam O'Connor (ANU): Introduction to Interactive Theorem-Proving with Isabelle
Week 2:
Sonia Marin (Birmingham): Intuitionistic Modal Logic
Chelsea Edmonds (UWA): Advanced Isabelle for Software Verification
Cláudia Nalon (Brasília): Resolution for Modal Logics and its Implementation
Gillian Russell (ANU): Barriers to Entailment
Vineet Rajani (UNSW): Modal Type Theories and Logical Relations
ORGANISATION
The logic summer school is organised by Ranald Clouston, Peter Hoefner, and Michael Norrish. Please direct all enquiries to lss.comp@anu.edu.au
My paper has now been officially published!
https://www.worldscientific.com/doi/10.1142/S0219061325500229
Alan Zimmerman
boosted
Formal verification — (machines constructing and checking mathematical proofs) — keeps getting better. Cobblestone ( @TaliaRinger https://arxiv.org/abs/2410.19940
) and other divide-and-conquer approaches now automate proofs we once thought unreachable.
But something feels different about where this is heading.
As we push automation forward, we’re starting to touch the edges of what a “proof” actually is — not just a verified computation, but a statement about what can’t be opposed.
I’m not sure the field has fully realized how close we’re getting to an ontological shift in what counts as proof itself.
Formal verification — (machines constructing and checking mathematical proofs) — keeps getting better. Cobblestone ( @TaliaRinger https://arxiv.org/abs/2410.19940
) and other divide-and-conquer approaches now automate proofs we once thought unreachable.
But something feels different about where this is heading.
As we push automation forward, we’re starting to touch the edges of what a “proof” actually is — not just a verified computation, but a statement about what can’t be opposed.
I’m not sure the field has fully realized how close we’re getting to an ontological shift in what counts as proof itself.
The official ads are now out for the #ANU #Logic Summer School, to be held in #Canberra , Australia from 1-12 December. https://comp.anu.edu.au/lss/
Paraphrasing a bit to fit in a toot:
OVERVIEW
The ANU Logic Summer School is an annual event that offers a two week long programme of lectures on modern logic, the foundational discipline of the information sciences. Topics include not only the science of reasoning but also computability theory, type theory and other tools for understanding processes, declarative programming, automatic proof generation, program verification and much more. The school is primarily geared at late undergraduate and masters students, but is open to all, including postgraduate and PhD students, postdocs, and participants from industry.
PROGRAMME
Week 1:
John Slaney (ANU): Foundations of Metalogic
Michael Norrish (ANU): Computability and Incompleteness
Peter Baumgartner (CSIRO): Overview of Automated Reasoning
Liam O'Connor (ANU): Introduction to Interactive Theorem-Proving with Isabelle
Week 2:
Sonia Marin (Birmingham): Intuitionistic Modal Logic
Chelsea Edmonds (UWA): Advanced Isabelle for Software Verification
Cláudia Nalon (Brasília): Resolution for Modal Logics and its Implementation
Gillian Russell (ANU): Barriers to Entailment
Vineet Rajani (UNSW): Modal Type Theories and Logical Relations
ORGANISATION
The logic summer school is organised by Ranald Clouston, Peter Hoefner, and Michael Norrish. Please direct all enquiries to lss.comp@anu.edu.au
theruran 💻 🌐 :cereal_killer:
boosted
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
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
But what if it's got more to do with logic than blame?
My feeling is:
1. It’s better to use the data we have to hand, as best we can. This involves focusing on & noticing outcomes.
2. It’s better to be cautious in potentially risky or even life-threatening situations (such as the one used in the famous study on this. Refs below).
3. It’s better if we all take some degree of responsibility in any situation we’re involved in.
⬇️