Trying out @FediTree
=> More informations about this toot | View the thread
Talk talk recording is now available on YouTube:
https://www.youtube.com/watch?v=NhFhJS4NHDM
and the slides on my homepage:
https://www.cse.chalmers.se/~patrikj/talks/2024-12_Jansson_OptiFun_Cambridge.pdf
I like how all the Cambridge talks are collected on a well-structured collection of pages: here is the link to the series: https://talks.cam.ac.uk/show/index/163292
and to the specific talk:
https://talks.cam.ac.uk/talk/index/225490
=> More informations about this toot | View the thread
On Friday I will give a talk in Cambridge (and on zoom): https://www.cst.cam.ac.uk/seminars/list/225490
The underlying topic
"Optimising Sustainable Energy with Functional Programming"
is the same as for my talk at Kellogg College, Oxford a month ago [1], but it is aimed at a bit more technical audience.
I will be in Cambridge from Thursday around 17 to Saturday around 12 in case anyone want to chat.
[1] https://patrikja.owlstown.net/posts/3188
=> More informations about this toot | View the thread
Here is Andreas Abel presenting a retrospective on 20 years of Agda (Implementors) Meetings. I have fond memories of the first few meetings back in the days when Ulf Norell and Nils Anders Danielsson were working on their PhD theses [and I was their thesis advisor]. I'm very grateful to all the developers and maintainers who have (and are still) spending time on making and improving Agda.
Fun fact: Ulf's PhD thesis [1] has now been cited [2] more than 1000 times (around 60 citations per year for 17 years).
[1] https://ncatlab.org/nlab/files/Norell-PracticalDTT.pdf
[2] https://scholar.google.com/citations?view_op=view_citation&hl=en&user=KEIhJYcAAAAJ&citation_for_view=KEIhJYcAAAAJ:u5HHmVD_uO8C
@ulfnorell
[#]Agda
@jesper
=> View attached media | View attached media
=> More informations about this toot | View the thread
ICFP 2024 videos are now online, and my presentation is here: https://www.youtube.com/watch?v=mxDjPTDwbGE
Many thanks to the volunteers and other professionals!
An earlier blog post about the paper is here:
https://patrikja.owlstown.net/posts/2013
and the text below
The technical meat of the paper is the specification and efficient implementation of the concept of "Level-p-complexity" for a Boolean function. The specification is itself executable (basically "generate all candidates, pick the least expensive") but with doubly exponential complexity. For the running example the set of candidates to sift through would be on the order of 10^100, thus completely intractable. The implementation combines a few algorithmic techniques:
The result is a computation which for the running example (the level-p-complexity of two-level iterated majority) finishes within seconds on a regular laptop.
The paper (and the code) is fully open access and I am currently supervising a pair of MSc students on follow-up work.
We'd be happy to hear your ideas for more follow-up work connected to the paper.
=> More informations about this toot | View the thread
Better late than never I have now added a 2nd blog post about the "Functional Programming and Climate Impact Research (FPClimate)" course:
https://patrikja.owlstown.net/posts/3285
The first blog post was here:
https://patrikja.owlstown.net/posts/2428
and my aim is to write a short post about each of the seminars.
To keep them together i set the blog dates as the dates of the seminars (2024-03-25, 2024-04-08, etc.).
We are considering having another course instance in the spring of 2025 - do get in touch if you are interested.
=> More informations about this toot | View the thread
I forgot to mention that I gave a research talk about parts of this in March this year:
"Tensor DSLs and Curved Space-Time"
https://www.youtube.com/watch?v=81XurNlv5cw
=> More informations about this toot | View the thread
Over the last few years, Jean-Philippe Bernardy and I have been exploring how to express tensor calculus (the Einstein notation, Penrose diagrams, and the categorical view) in Haskell. The paper is under review and we have just uploaded a new version to arXiv, after receiving lots of good feedback from reviewers (and acting on the 86 suggestions...). https://arxiv.org/abs/2312.02664
Now hoping it will soon be accepted for the journal.
(Here is an earlier blog post from when it was first submitted to JFP: https://patrikja.owlstown.net/posts/2002-domain-specific-tensor-languages )
=> More informations about this toot | View the thread
An undergraduate student asked me to explain dependent types, and I had the opportunity to demo this little Agda example again:
https://youtu.be/sFyy9sssK50?si=cuN48W42oxbq_d2W
I make a normal syntax datatype for simple expressions (0,1,+,*), then implement three alternative semantics: as natural numbers, as finite types, and as enumerations of the values of those types.
I hope others also find it illuminating.
=> More informations about this toot | View the thread
The video recording is now available on YouTube:
https://www.youtube.com/watch?v=ZIP0FMDSDOA&list=PLf5C73P7ab-4OCYhM1STDCgki_pUTD7w8&index=9
=> More informations about this toot | View the thread
Yesterday I delivered a talk at Kellogg College, Oxford on "Optimising Sustainable Energy with Functional Programming". The slides are now available here:
https://www.cse.chalmers.se/~patrikj/talks/Jansson_OptiFun_Kellogg_2024.pdf
and a recording here
https://www.youtube.com/watch?v=ZIP0FMDSDOA&list=PLf5C73P7ab-4OCYhM1STDCgki_pUTD7w8&index=9
It was basically a popular science talk / lecture on optimisation of (numerical) simulations. I presented two motivating example domains: fusion energy and climate impact research and went on to explain some of the concepts and techniques. Part one was about cost functions and Bayesian optimisation (balancing exploration and exploitation). Part two was about true multi-objective optimisation where the Pareto-front captures trade-offs between conflicting objectives. Finally I presented a bit about ongoing and future research directions: Pareto front computation using adaptive mesh refinement, and applications to optimal climate decisions.
Blog post:
https://patrikja.owlstown.net/posts/3188-talk-optimising-sustainable-energy-with-functional-programming
=> View attached media | View attached media
=> More informations about this toot | View the thread
Two BSc project proposals:
https://patrikja.owlstown.net/posts/3189
One about "Which Climate Decisions Matter Most?" and one on "DSLs of Maths for other courses".
While these proposals are specifically targeted at a big third year BSc project course here in Gothemburg, I'm also interested in related projects on the graduate (MSc- or PhD-)level.
=> More informations about this toot | View the thread
Upcoming talk announcement:
https://www.eventbrite.co.uk/e/optimising-sustainable-energy-with-functional-programming-tickets-1064147747559?aff=oddtdtcreator
"Optimising Sustainable Energy with Functional Programming"
=> View attached media | View attached media
=> More informations about this toot | View the thread
I've just submitted a grant proposal on "Theories and Tools for Climate Policy Exploration"
https://patrikja.owlstown.net/posts/3101-submitted-grant-application-theories-and-tools-for-climate-policy-exploration
We want to use functional programming, domain-specific languages, dependent types, etc. from programming languages research in combination with sequential decision problems, optimal policies under uncertainty, and Pareto fronts from climate impact research.
Do get in touch if you think this line of works seems interesting!
I submitted similar applications last year but they were all rejected. Let's hope that submitting from Oxford increases my chances;-)
=> View attached media | View attached media | View attached media
=> More informations about this toot | View the thread
My "Visiting Fellow" page is now up at Kellogg college here in Oxford:
https://www.kellogg.ox.ac.uk/our-people/patrik-jansson/
I'm visiting @jer_gib Oct-Nov-Dec and I'm eager to learn new things, connect to new people, and contribute with some of what I've learned over the years.
Do get in touch if you think my profile contains something you think could complement your research project / network / proposal / paper / etc.
=> More informations about this toot | View the thread
Just arrived in Oxford for a 3-month sabbatical hosted by @jer_gib ! Staying at Postmasters' Hall, Merton college, where my wife, Professor Tünde Fülöp is visiting fellow.
=> View attached media | View attached media | View attached media
=> More informations about this toot | View the thread
Now on my way to the #ICFP2024 conference in Milan, Italy.
=> More informations about this toot | View the thread
Preparing for my talk at ICFP [1]:
"Level-p-complexity of Boolean functions using thinning, memoization, and polynomials" (joint work with Julia Jansson)
Code and earlier presentations are available on GitHub [2].
For this talk I have to rethink what is important, because the slot is just 15min + 3min questions and I have earlier presented it at a seminar [3] in around an hour (including questions).
[1] https://icfp24.sigplan.org/details/icfp-2024-jfp-first-papers/4/Level-p-complexity-of-Boolean-functions-using-thinning-memoization-and-polynomials
[2] https://github.com/juliajansson/BoFunComplexity
[3] https://youtu.be/Z0cACMp8_hk
[#]Haskell
[#]Agda
=> More informations about this toot | View the thread
Come and work with us!
The Logic and types group of the Department of computer science and engineering, Chalmers and Gothenburg University, is recruiting to a 3-year postdoc position to work with dependent type theory extended with univalence and higher inductive types.
For more information about the position and how to apply for it, please follow this link
https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=35073
Deadline for application is 2024-09-17.
Please do not hesitate to contact us if you have any questions.
[#]Agda #HOTT
=> More informations about this toot | View the thread
Atharva Sehgal, PhD student, U Texas
Neurosymbolic programming (NSP) is an emerging area of computing that bridges deep learning and program synthesis. Like in classical machine learning, the goal here is to learn functions from data. However, these functions are represented as programs that use neural network modules as well as symbolic primitives and are induced using a mix of symbolic reasoning and statistical methods.
In this talk, I will give an elementary introduction to NSP and show how methods in this area have natural applications in accelerating scientific discovery. Specifically, I will describe a general framework for synthesizing programs by leveraging large language models (LLMs) to learn concept libraries concept guidance. Using applications in astronomy and ornithology, I will show how NSP offers natural ways of incorporating prior knowledge into data-driven scientific discovery and interpreting automatically discovered knowledge. I will conclude with a discussion of some of the open technical challenges in NSP in general and NSP-for-science in particular.
https://atharvas.net/
=> More informations about this toot | View the thread
=> This profile with reblog | Go to patrikja@functional.cafe account This content has been proxied by September (3851b).Proxy Information
text/gemini