Now I'm a big fan of refinement type. But they don't sit all that well with me because most examples I've seen could be manipulated into ADTs (read the previous post backwards).

Does anyone know of some work that does this manipulation? Or somehow sets some constraints on when you can't express a refinement types using 1,0,+,*, and mu (recursive) types?

Again, my suspicion is that it has to do with regular languages since 1,0,+,*,mu is a #Kleene algebra (right?)

What are people's thoughts/experiences with #Kleene?

https://gyptazy.com/howto-kleene-as-a-container-management-platform-for-freebsd/

#FreeBSD

#Docker alike container management on #FreeBSD? Let's have a look at #Kleene - which works very similar to Docker and makes the shift for Linux users even easier to #Jails without having deeper knowledge but by benefiting of all the features on Jails.

#klee #kleened #bsd #runbsd #linux #container #howto #devops #community #jails #freebsdjail #container #containerization #jailmanager #manager #jls

https://gyptazy.com/howto-kleene-as-a-container-management-platform-for-freebsd/

#Kleene's theorem: The set of regular languages, the set of NFA-recognizable languages, and the set of DFA-recognizable languages are all the same.

#Logic folks
In
R : φ1*φ2* ... *φn =0
R acts as logical
#kleene #godel #recursion

#Kleene was supposed to develop arithmetic from church numerals, he ended up finding that unlike succ n, church's lambda calculus has no notion for prev n.
His fix was to start the number line with pair 0,0 . With An extra 0, and map +1 the entire sequence S , to get a regular

#Kleene rosser found the logical paradox in the #lambdacalculus, #church was working at the time, when #godel lectured on incompleteness in ias - Princeton
#Haskell curry was doing almost same thing as church, under #Hilbert
syntactically substituting one formula in another

#Kleene's #recursive realizability proofs of intuitionistic arithmetic: recursive function f( proof of a formula expressing that recursive function "realizes", i.e. correctly instantiates the disjunctions) + existential quantifiers of the initial formula st formula gets true

#Kleene Turing machine T tape : "a linear 'tape' t potentially infinite p in both ways To access memory on t, a T moves a read head along it in finitely many steps s: t is only p as while there is always ability to take next s infinity itself is never actually reached #limit

#Kleene–Brouwer order of a well-founded computation tree is itself a recursive well-ordering, and at least as large as the ordinal assigned to the tree, from which it follows that the levels of this hierarchy are indexed by #recursive ordinals

- In predicate transformers semantics, invariant and variant are built by mimicking #kleene fixed point theorem

Tree T :
Descriptive set theory:
A set of Finite sequences S that is closed under prefix ops. Parent in tree of any seq is shorter seq formed by removing its final element.
Any S can be augmented to form T #Kleene #Brouwer order is a natural ordering for T
generalizing