Jesper Agdakx

@kha @mattam @beta We just don't solve these kind of equations in Agda. Here's the example with the error in comment: gist.github.com/jespercockx/fc

I suppose it takes a different style of coding, but I don't hear Agda complain about it too often (but perhaps the people who would complain are all using Coq or Lean instead).

We do have a (relatively recent) option --lossy-unification which enables a first-order unification heuristic (and makes the example pass) that some people seem to like, so there is definitely more work to be done.

1
Jesper Agdakx boosted
*
Deyan Ginev

In one day - one day! - of going open source, the Typst typesetting system passed 5,000 stars on Github.

If you ever needed evidence that there is a real hunger for a TeX replacement, this is it.

github.com/typst/typst

1+
Jesper Agdakx

@jonmsterling Wow, congratulations! You should tell me one day the trick to skipping the assistant professor step ;)

0
Jesper Agdakx boosted
Jon Sterling

I'm overjoyed to announce that I will be starting as an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge this fall!

1+
Jesper Agdakx boosted
Amélia Liao

@jonmsterling i think the human brain can only take so much type theory before it needs a day off to nap or something

0
Jesper Agdakx boosted
Cory Doctorow's linkblog

*Red Team Blues* is my next novel, a #PostCyberpunk anti-finance finance #thriller; it's a major title for my publishers Tor Books and Head of Zeus, and it's swept the trade press with starred reviews all 'round. Despite all that, #Audible will not sell the #audiobook. In fact, Audible won't sell *any* of my audiobooks. Instead, I have to independently produce them and sell them through Kickstarter:

kickstarter.com/projects/docto

1/

1+
Jesper Agdakx boosted
Conor Mc Bride

I'm too tired just now to tell you what little I know about the beginnings of an answer to this question but...

Orbits. What are orbits? Never mind what groups are or how they act on whatever they act on: what are the orbits? What is it to be a system of orbits and stabilisers that comes from a group acting on a set?

I feel like Ptolemy having a go at Copernicus in 2023.

1
Jesper Agdakx boosted
José A. Alonso

Certified logic-based explainable AI (The case of monotonic classifiers). ~ Aurélie Hurault & Joao Marques-Silva. hal.science/hal-04031193/docum #ITP #Coq #XAI

0
Jesper Agdakx boosted
Kevin Buzzard

Daniel J. Velleman has translated parts of his classic text "How to prove it" into Lean 4!

djvelleman.github.io/HTPIwL/

"How to prove it in Lean" goes through examples in the original book, and discusses how they can be proved in Lean. He also talks about how Lean's use of type theory rather than set theory affects this kind of basic mathematics, and furthermore gives clear installation instructions for anyone who wants to play along at home!

0
Jesper Agdakx

@MartinEscardo
TU Delft already has a separate department of Intelligent Systems, and will soon have a separate master on Data Science and Artificial Intelligence Technology. But this does not seem to prevent AI research from also happening elsewhere.

0
Jesper Agdakx

Proudly helping to avert the AI apocalypse by proposing student projects, thus enabling smart students to spend their brain cycles on building type systems instead of AI models.

(This toot brought to you by several students telling me they found one of my proposals by searching for anything that did not have "AI" or "machine learning" in the description.)

1+
Jesper Agdakx boosted
Sebastian Ullrich

@beta @mattam This is especially true because the issue disproportionately affects *invalid* programs, e.g. during editing. Which, yes, we do not have a good database of either.

1
Jesper Agdakx boosted
Wouter Swierstra :verified:

We're hiring an assistant professor in CS Education! Utrecht is a great place to live & work: uu.nl/en/organisation/working-

1
Jesper Agdakx

@ionchy This feels like part one of a meme where the second part involves you saying "Oh no" while being crunched under a huge pile of eta-expanded terms.

1
Jesper Agdakx boosted
Simon Willison

Got access to Google Bard! I'm pleased to report that it is ethically opposed to necromancy

1+
Jesper Agdakx boosted
*
Peter Mosses

The Proceedings of EVCS – the Eelco Visser Commemorative Symposium – have now been published online, open access:

dagstuhl.de/dagpub/978-3-95977

0
Jesper Agdakx

@beta I'm not sure I see what it means to "note how arguments are used within the function". Could you give an example where Coq or Lean or Agda could be smarter?

1
Jesper Agdakx

@mattam @beta @kha Configurable levels of abstraction are coming to an Agda near you Soon (TM): github.com/agda/agda/pull/6354

1
Jesper Agdakx boosted
*
Sebastian Ullrich

I was a happier man before I knew that Coq and Lean unification is inherently exponential (and practically significantly so, especially on failure) because of backtracking

Excerpts from §2 of @beta & @mattam: A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading

1
Jesper Agdakx

@mattam @beta @kha The problem here is not unification per se but rather backtracking. It is possible to implement a unification algorithm that only makes forced steps so it never needs to backtrack, and still have a usable system.

1+
Show older

agda

9
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.

Resources

Developers

What is Mastodon?

types.pl

More…

v3.5.5+types · Privacy policy