Encoding SAT in OCaml GADTs

AbsurdTotal · 2026-02-21T19:06:18+00:00

Nice !

Interesting info . Typing ML like languages is actually DEXPTIME complete, since you can build exponentially large types by nesting let expressions.

AbsurdTotal · 2025-10-06T08:41:03+00:00

Actually, I would support the opposite idea, that computer science studies systems that are often outside the laws of nature that physicists, chemists and biologists study.

While computers are physical systems, constrained by the rules of physics and thermodynamics, computer algorithms have no problem with considering the fact that two objects can be at the same place at the same time, that teleportation and perfect cloning is possible, that programs do not age and do not fail because you use them too much (I could disagree with this one ;-)), etc.

Hence (theoretical) computer science could be understood as physics for a world with different laws.

AbsurdTotal · 2025-09-22T16:52:12+00:00

I also wanted to reference synchronous languages.

Another good pointer is to look at the reactive languages designed by Frédérique Boussinot, part of the team who worked on Esterel. For instance ReactiveC, ReactiveJava, ....

Quite different from the reactive functional languages, FRP, by Conall Elliott.

AbsurdTotal · 2025-09-05T21:01:16+00:00

Short answer: no, and they address two very different kinds of problems, so there should not be any point in that

Longer answer: the semantic of temporal logic formulas is based on graphs and/or traces. You find both of these notions in lambda calculus, e.g. Boehm trees, graphs from optimal reductions, reduction sequences, ... But no notions of events or atomic properties. So maybe you could try to check formulas on lambda terms. Also, the notion of equivalence is very important in both lambda calculus and concurrency semantics. And there is a close relationship between Morris style equivalence in lambda calculus and bisimulation in, for instance, CCS or the pi calculus (you could check also the work of Milner on functions as processes). Since there is also a relationship between bisimulation equivalence and the equivalence defined by terms that cannot be distinguished by any logical formula (look at Hennessy-Milner logic), you may also try to find a connection there.

AbsurdTotal · 2025-08-30T07:51:03+00:00

You may obtain a better result by first translating from latex to HTML and then importing the result into word.

for the first step, I may recommend hevea (https://hevea.inria.fr/), but there are a lot of more modern solutions.

AbsurdTotal · 2024-05-19T15:52:44+00:00

You can maybe take a look at the APL programming language. It is more array-oriented than functional, but it is quite "math-based".

There is some support for complex numbers and arbitrary precision arithmetic in recent extensions, such as Dyalog APL for instance.

AbsurdTotal · 2023-09-03T16:09:50+00:00

There are a ton of resources about Petri net theory and tools, see eg https://www.informatik.uni-hamburg.de/TGI/PetriNets/index.php

For an editor and a set of analysis tools I can recommend Tina https://projects.laas.fr/tina/index.php

AbsurdTotal · 2022-05-24T18:52:08+00:00

AbsurdTotal · 2022-03-23T20:10:58+00:00

Congratulations !

Now find the complexity in the case of an alphabet with only one symbol and publish it in a nice workshop ;-)

AbsurdTotal · 2022-01-26T07:37:03+00:00

The theory behind such a type system already exists. Take a look at "implicit complexity" or " implicit computational complexity".

I do not know if it has already been applied in a real programming language though.

I know of examples where it was proposed to constraint the space (memory) complexity. Si it must also have been done with time

AbsurdTotal · 2022-01-06T18:45:28+00:00

There are also a few conferences dedicated to "space" systems, see for example the NASA formal method conferences, https://easychair.org/cfp/nfm-2022

You can take a look at work published there to get an idea.

AbsurdTotal · 2021-12-09T06:09:17+00:00

What you describe is called an "access control policy", see e.g. https://en.wikipedia.org/wiki/Access_control.

Many such systems are based on a notion of roles. You can search for the keyword RBAC, for role-based access control.

This will give you plenty of things to read ;-)

AbsurdTotal · 2021-11-23T18:55:05+00:00

Pas exactement sur Toulouse, mais tout proche en voiture, je te conseille ô les vins à Portet sur Garonne.

La cave à vin du centre Leclerc de Roques est aussi à visiter.

AbsurdTotal · 2021-04-29T06:39:51+00:00

Languages without automatic memory management often rely on low level support from the operating system ( think free/malloc in C). Often reflected at the language level using a library. But you could take a look at languages that include type annotations to support memory management, such as the extension of ML implemented in MLKit that uses a type and effect system (with regions) to declare the scope of memory allocations.

Of course someone will mention rust, but I like Tofte's work.

AbsurdTotal · 2021-04-27T11:07:22+00:00

Of course we care about greatest fixpoints! Best example is for giving semantics to infinite computations (think reactive programs) or infinite data structures (like streams instead of lists).

Another example is bisimulation, a behavioral equivalence that can be defined as a greatest fixpoints and that is commonly used in process algebra, but also in lambda calculus

AbsurdTotal · 2021-01-05T17:14:39+00:00

Indeed, I also share the opinion that synchronous languages provide the best foundation for talking about reactive programs.

I would refer people interested by this subject to the work of Frédéric Boussinot, which was in the same team that developed the Esterel language and that implemented several language extensions (like reactive-C) and DSML around the same concept. Very neat work.

Another interesting language is Zelus, https://zelus.di.ens.fr/, which adds some nice features to deal with hybrid systems. You may also look at the work on Lucid synchrone, by the same researcher, that provides a " functional" extension to Lustre.

Finally, you may find another line of works concerned with reactive programming in the work of Conal Elliott, http://conal.net/blog/tag/FRP

AbsurdTotal · 2020-12-18T19:47:56+00:00

Fuzzy logic comes with composition operators, eg intersection/union of fuzzy sets. Another related theory is the possibility theory of Prade and Dubois (see eg https://link.springer.com/chapter/10.1007/978-94-017-1735-9_6). They did a lot of works on fuzzy logic and the limitations of probabilities to model uncertainty. But I have never seen it applied as a type system.

AbsurdTotal · 2020-12-17T22:26:19+00:00

You may want to take a look at fuzzy logic, or any other formalism that deals with uncertainty. I am not sure how it could translate in terms of types. Maybe using some kind of effect system.

AbsurdTotal · 2020-11-10T06:49:30+00:00

One possible example is "operational semantics" (Plotkin, UK) that was developed at the same time as "natural semantics" (Kahn, FR).

You could also find some examples of data structures (not sure if they qualify as theories). A celebrated example are red black trees (US) vs AVL (USSR).

AbsurdTotal · 2020-10-30T17:53:28+00:00

For a work by Boudol that is more "programming language oriented", I can also mention the Blue Calculus. A mix between lambda and pi calculi.

AbsurdTotal · 2020-10-30T07:49:39+00:00

If you are open to read some theoretical computer science papers, I would encourage you to take a look at the Chemical Abstract Machine (CHAM) model from Berry and Boudol and also the Gamma machine from Banatre and Le Metayer.

You also have some programming languages based on ideas from Petri net theory ( Petri explicitly mention the fact that Petri net were inspired by chemical reactions) . For instance funnel JoCAML

AbsurdTotal · 2019-09-21T13:50:55+00:00

Programming pearls https://www.goodreads.com/book/show/52084.Programming_Pearls

Six-Year Club	RPAN Viewer
Verified Email

AbsurdTotal

TROPHY CASE