Papers and articles

Publications that I came across one time or the other.

2024

November

August

Lilac - Li, Ahmed, Holtzen (PLDI'23)

Look up:

Dlugosch, P., Brown, D., Glendenning, P., Leventhal, M. and Noyes, H., 2014. An efficient and scalable semiconductor architecture for parallel automata processing. IEEE Transactions on Parallel and Distributed Systems, 25(12), pp.3088-3098.

this architecture exceeds the capabilities of high-performance FPGA-based implementations of regular expression processors.

Offtopic:

Nourian, M., Wang, X., Yu, X., Feng, W.C. and Becchi, M., 2017. Demystifying automata processing: GPUs, FPGAs or Micron's AP?. In Proceedings of the International Conference on Supercomputing (pp. 1-11).

Micron's AP delivers throughputs, pattern densities, and preprocessing times that are intermediate between those of FPGAs and GPUs, and it is most suited for applications that use datasets consisting of many small NFAs with a topology that is fixed and known a priori.

Associated masters thesis: https://mospace.umsystem.edu/xmlui/bitstream/handle/10355/59977/research.pdf?sequence=2&isAllowed=y

Barrière, A. and Pit-Claudel, C., 2024. Linear Matching of JavaScript Regular Expressions. Proceedings of the ACM on Programming Languages, 8(PLDI), pp.1336-1360.

April

Design Patterns for Parser Combinators (Functional Pearl) - Jamie Willis, Nicolas Wu

Cohen, C., Crance, E. and Mahboubi, A., 2023. Trocq: Proof Transfer for Free, With or Without Univalence. arXiv preprint arXiv:2310.14022.

Presented at ESOP 2024.

Trocq implementation incorporate CoqEAL along with support for univalent axioms if needed.

February

Gay, S.J., 2020. Cables, trains and types. From Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement, pp.3-16.

Vericert https://yannherklotz.com/papers/fvhls_oopsla21.pdf https://github.com/ymherklotz/vericert

C -> compcert -> Verilog

Call-by-push-value: Paul Blain Levy https://dl.acm.org/doi/10.1145/3537668.3537670

Dbts:

—

Coq implementation: https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl_2018_Call-By-Push-Value.pdf

—

https://qmro.qmul.ac.uk/xmlui/bitstream/handle/123456789/4742/RR-01-03.pdf?sequence=1

Harper, R., Honsell, F. and Plotkin, G., 1993. A framework for defining logics. Journal of the ACM (JACM), 40(1), pp.143-184.

3 levels:

Notations:

DBT:

January

Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming - Sam Lindley, Conor McBride

—

Haskell’s dependent ∀·quantifier is for implicit and exclusively static things

I guess, here the authors are talking about forall a. a thing.

— Why was a separate Natty type needed for splitting a vector into two vectors?

Haskell

class Collects es e where
  insert :: e -> es -> es
  element :: e -> es -> Bool

instance Eq a => Collects (a -> Bool) a where
  insert e f = (\x -> x==e) || (f x)
  element e f = f e

instance Eq a => Collects [a] a where
  insert e l = e : l
  element e l = elem e l

instance (Hashable e, Collects es e) => Collects (HashTable es) e where
  insert e es = 
  element e es =

—

Vector: Something like this would be nice..

data Vector a n
  = Nil
  | Cons a (Vector a (n-1))


{-
λ> Cons 3 Nil
Cons 3 Nil :: Num a => Vector a n

But the `n' value is useless in this form..
-}

This one works:

data Vector :: Nat -> Type -> Type where
  Nil :: Vector 0 a
  Cons :: a -> Vector n a -> Vector (Suc n) a

-- https://hackage.haskell.org/package/clash-prelude-1.8.1/docs/src/Clash.Sized.Vector.html#Vec

2023

November

Kami

Conventions:

Module consists of:

Krishnaswami, N.R. and Yallop, J., 2019, June. A typed, algebraic approach to parsing. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 379-393).

the old observation that the context-free languages can be understood as the extension of regular expressions with variables and a least-fixed point operator (aka the μ-regular expressions

October

Cohen, C., Dénès, M. and Mörtberg, A., 2013, December. Refinements for free!. In International Conference on Certified Programs and Proofs (pp. 147-162). Cham: Springer International Publishing.

Types of refinement:

Steps for data refinement:

  1. Relate: Make a relation between proof-friendly data representation with the computation-friendly representation
  2. Parametrize: Make an abstract data type parametrized by data representation.
    • With abstract types and basic operations
  3. Instantiate the abstract type with proof-friendly representation and prove its correctness
  4. Use parametricity of the abstract type to show that the computation-friendly repr is also correct

–

Refinement relations:

Examples:

—

Need for parametricity:

Proving correctness directly on computation-oriented types is precisely what we are trying to avoid

R: A -> B
R': A' -> B'
R ==> R': (A -> A') -> (B -> B')

—

Dbts:

Bourgeat, T., Clester, I., Erbsen, A., Gruetter, S., Singh, P., Wright, A. and Chlipala, A., 2023. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the ACM on Programming Languages, 7(ICFP), pp.108-124.

Macedo, H.D. and Oliveira, J.N., 2013. Typing linear algebra: A biproduct-oriented approach. Science of Computer Programming, 78(11), pp.2160-2191.

Dénès, M., Mörtberg, A. and Siles, V., 2012, August. A refinement-based approach to computational algebra in Coq. In International Conference on Interactive Theorem Proving (pp. 83-98). Berlin, Heidelberg: Springer Berlin Heidelberg.

having the size of matrices encoded in their type allows to state concise lemmas without explicit side conditions, but it is not always flexible enough when getting closer to machine-level implementation details.

It is worth noting that we could have stated all our morphism lemmas with the converse operator (from concrete matrices to abstract ones). But these lemmas would then have been quantified over lists of lists, with poorer types, which would have required a well-formedness predicate as well as premises expressing size constraints. The way we have chosen takes full advantage of the information carried by richer types.

More reading:

–

T: Type
M N: matrix A rows cols
meq: seq (seq T) -> seq (seq T) -> bool
───────────────────────

let Mc := seqmx_of_fun M in
let Nc := seqmx_of_fun N in
reflect (M=N) (meq Mc Nc)

September

Agnishom Chattopadhyay (Rice uni) MTL paper

Kanabar, H., Vivien, S., Abrahamsson, O., Myreen, M.O., Norrish, M., Pohjola, J.Å. and Zanetti, R., 2023. PureCake: A Verified Compiler for a Lazy Functional Language. Proceedings of the ACM on Programming Languages, 7(PLDI), pp.952-976.

HOL4 verified compiler from a haskell-like language to cakeml.

Landi, W., 1992. Undecidability of static analysis. ACM Letters on Programming Languages and Systems (LOPLAS), 1(4), pp.323-337.

Code:

August

A tutorial on the universality and expressiveness of fold - Graham Hutton (1999)

recursion and induction are the primary tools for defining and proving properties of program

New(ish) stuff:

To read:

difflist paper Hughes

abstr: CONCR -> ABSTR
concr: ABSTR -> CONCR

∀a:ABSTR,
  abstr (concr a) = a

Dijkstra about teaching:

General:

Dijkstra, E.W. 1979. On the foolishness of 'natural language programming'. In: Bauer, F.L., et al. Program Construction. Lecture Notes in Computer Science, vol 69. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014656

(Only 3 pages)

Probably still true:

some people found error messages they couldn't ignore more annoying than wrong results, and, when judging the relative merits of programming languages, some still seem to equate "the ease of programming" with the ease of making undetected mistakes.

—

About good notations:

Greek mathematics got stuck because it remained a verbal, pictorial activity, Moslem "algebra", after a timid attempt at symbolism, died when it returned to the rhetoric style, and the modern civilized world could only emerge - for better o2 for worse– when Western Europe could free itself from the fetters of medieval scholasticism

—

About advantage of formal langauges:

The virtue of formal texts is that their manipulations, in order to be legitimate, need to satisfy only a few simple rules; they are, when you come to think of it, an amazingly effective tool for ruling out all sorts of nonsense that, when we use our native tongues, are almost impossible to avoid.

—

Funny, yet meaningful.

From one gut fesling I derive much consolation: I suspect that machines to be programmed in our native tongues –be it Dutch, English, American, French, German, or Swahili– are as damned difficult to make as they would be to use.

Dijkstra 'Humble progammer'

General:

—

silence their doubts by observing how many of these machines have been sold, and derive from that observation the false sense of security that, after all, then cannot have been that bad. But upon closer inspection, that line of defense has the same convincing strength as the argument that cigarette smoking must be healthy because so many people do it.

—

About compatibility with old code constraining new ideas, here with respect to FORTRAN:

FORTRAN'S tragic fate has been its wide acceptance, mentally chaining thousands and thousands of programmers to our past mistakes. I pray daily that more of my fellow programmers may find the means of freeing themselves from the curse of compatibility.

—

About learning from problems of FORTRAN and PL/I:

there is no point in making mistakes unless thereafter we are able to learn from them.

—

*Those who want really reliable software will discover that they must find means of avoiding the majority of bugs to start with*
…
If you want more effective programmers, you will discover that they should not waste their time debugging - they should not introduce the bugs to start with.

—

Today a usual technique is to make a program and then to test it.

But: program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness. But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmer's burden. On the contrary: the programmer should let correctness proof and program grow hand in hand.

Datatype à la carte - 2008

data Expr f = In $ f (Expr f)
data Val e = Val Int
type IntExpr = Expr Val


data Expr f = In (f (Expr f))
data Val e = ValC Int
type IntExpr = Expr ValC

In (ValC _)

On-the-fly Verification of Linear Temporal Logic 1999 LaBRI Bordeaux

Peled, D. and Havelund, K., 2019. Refining the safety–liveness classification of temporal properties according to monitorability. Models, Mindsets, Meta: The What, the How, and the Why Not? Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, pp.218-234.

Lamport's ?? New dual
Safety guarantee
Liveness Morbidity

Ref papers to be read:

Pike, L., Wegmann, N., Niller, S. and Goodloe, A., 2013. Copilot: monitoring embedded systems. Innovations in Systems and Software Engineering, 9, pp.235-255.

Original copilot paper:

RV paper from ICFP'23

systematic and rigorous evidence that can be audited.

Perez, I., Dedden, F. and Goodloe, A., 2020. Copilot 3 (No. NF1676L-35996).

This is not the paper that introduced the tool. This seems to be an improvement over earlier versions.

https://github.com/Copilot-Language/copilot

—

Motivation for this paper:

monitors for hard real-time avionics should not afefct the system under observation in a way that changes the functionality of the system, requires re-certification, interferes with timing, or exhausts size, weight, and power (SWAP) reserves.

—

Runtime verification (RV) [Havelund and Goldberg, 2008, Goodloe and Pike, 2010, Bartocci et al., 2018] is a verification technique that has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify or fully test. In RV, the system is monitored during execution, to detect and respond to property violations that take place during the actual mission. RV detects when properties are violated in runtime, so it is not a proof of correctness, but a significant improvement over testing alone.

—

The language also relies on dependent types, to enable safe use of non-primitive data structures, like structs and arrays.

—

Temporal logic languages generally vary in the logic they are based on, the temporal operators they support and in their model of time (e.g., continuous vs discrete, linear vs branching, future and/or past, etc.). These aspects impact what formulas can be expressed, which ones are true or false, what information is needed to evaluate them, and how efficiently we can do so.

In Copilot, we opt for implementing Bounded LTL, a variant of LTL in which the amount of time into the future that is observable is bounded in each application of a temporal operator.

—

:DBT: Examples of properties that are not expressible in LTL: a property that is true at every alternate time step.

some properties are known not to be expressible in LTL, such as, for example, a formula that is true at every other sample, but they can be expressed in Copilot due to the existence of delays and recursion.

In LTL, the next operator (ie, X) is essentially a delay, right?

—

Isn't MTL ⊆ LTL though? Ranges can be made in LTL as well although the formula would be far from concise.

Braibant, T. and Pous, D., 2010, July. An efficient Coq tactic for deciding Kleene algebras. In International Conference on Interactive Theorem Proving (pp. 163-178). Berlin, Heidelberg: Springer Berlin Heidelberg.

matrices over a Kleene algebra form a Kleene algebra

Coquand, T. and Siles, V., 2011, December. A decision procedure for regular expression equivalence in type theory. In International Conference on Certified Programs and Proofs (pp. 119-134). Berlin, Heidelberg: Springer Berlin Heidelberg.

Firsov, D. and Uustalu, T., 2013, December. Certified parsing of regular languages. In International Conference on Certified Programs and Proofs (pp. 98-113). Cham: Springer International Publishing.

Note that instead of the Kleene star (*) we use plus (_+). This is more convenient for us and does not restrict generality, as star is expressible as choice between the empty string and plus. Now, we need to specify when a string (an element of type List Σ) is

Notations used:

Star is defined in terms of ε and Char.

Matrix defined in terms of a commutative semiring.

Misc thoughts

Project thoughts:

lang deriv - Conal Elliott (ICFP 2021)

𝒟: says what can come after 'u'

-- Derivative
𝒟: ([A] -> B) -> [A] -> ([A] -> B)
𝒟 f u = λv => f (u++v)

I guess we can think of [A] -> B being a language. Language involving only the [A] given, I suppose?

For languages, 𝒟 P u is the set of u-suffixes from P, i.e., the strings v such that u ++ v ∈ P.

:DBT: Shouldn't it be 'u-prefixes from P'?

Plotkin, G.D. and Pretnar, M., 2013. Handling algebraic effects. Logical methods in computer science, 9.

Combinator parsing: A short tutorial - S. Doaitse Swierstra

Relevant for a good library:

June

TU Delft agda2hs MSc thesis

Ref:

Coq: Best macro assembler

Dbt:

Possibly related code repos and links:

Tag-Free Garbage Collection for Strongly Typed Programming Languages - Benjamin Goldbe

Traditionally, garbage collection (and dynamic type checking) required each datum to be tagged with type information (see [Ungar86] for description of various tagging schemes). During garbage collection, the tag of each datum is examined in order to determine how the datum should be handled. Naturally, whether the datum is a number, pointer, structure, or closure will determine how the object is treated by the collector.

Dbt:

Chlipala, A., 2007. A certified type-preserving compiler from lambda calculus to assembly language. ACM Sigplan Notices, 42(6), pp.54-65.

Dbts:

Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S. and Zdancewic, S., 2005. Mechanized metatheory for the masses: the PoplMark challenge. In Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings 18 (pp. 50-65). Springer Berlin Heidelberg.

POPLMark challenge

Dreyer, D. and Pierce, B.C., 2022. On being a PhD student of Robert Harper. Journal of Functional Programming, 32, p.e3.

The trick was doing this in a principled way

Towards the end of my graduate career, I had figured something out and was excited to show Bob. I went up to his office but couldn’t find him. In fact, he disappeared for a whole week. (I later found out he was trying to solve all of the puzzles in the "Myst" CD-ROM game that was all the rage back then.) When I finally tracked him down, I started writing on the white board and got about half-way through explaining whatever it was that so excited me. Bob kept interrupting me with questions. I got so frustrated that I finally just threw the white board marker at him and yelled at him to “Shut up!” At that point, he leaned back in his chair, smiled, and said, "Now you’re ready to graduate."

one day in grad school I revealed to Bob that I didn’t know anything about logical relations. In typical Bob fashion, he was very surprised and gave me a hard time for not having already educated myself about this fundamental thing that he thought every student should know. To rectify this lapse in my education, he spent the afternoon giving me a private lesson in his office about logical relations, starting with Tait’s method for proving strong normalization of the simply-typed λ-calculus, and then Girard’s method for proving the same of System F. If I recall correctly, he described these as "book proofs", a reference to Paul Erdös's idea of proofs so beautiful that they belonged in God’s book of perfect mathematical proofs

Bob has embraced the motto, "Dare to be irrelevant." I think that, while catchy and provocative, this slogan is but one instance of a broader lesson that I took away from Bob’s research and mentorship, namely: "Dare to think for yourself. Question the conventional wisdom. If everyone else is going one direction, go the other way. It’s OK to be weird."

Far more valuable though, I think, was a rigorous education in the value of a kind of clarity of thought, and co-equally of communication. Bob was never satisfied with something that just worked. It had to obviously work, and it had to explain by its very expression how it worked. The occasional marathon sessions in Bob's office working through a problem were as much about arriving at an explanation for a solution as at the solution itself. This appreciation for thinking and communicating clearly was almost certainly by far the most valuable thing I took away from my time with Bob

It took me several months to rewrite the introduction because I had to first familiarize myself with a century of mathematics. Only then could I truly understand where my dissertation stood in the universe of all knowledge. I feel privileged. His high standards elevated me

Bob’s advice was that it takes 10 years to gain expertise in a new field, and that I should be ready for that. I think it depends. If you’re lucky enough to have an advisor like Bob, that time frame can be drastically reduced.

not just a boring version of programming where rules prevented you from having fun and being creative. This was a better version of programming that I didn’t know about yet.

Communicating about research, both in written and spoken form, is a critical part of being a researcher.

conferences were for meeting new people!

research can and should be motivated by teaching. If something important is too difficult or confusing to explain to students, that’s a sign that the underlying ideas can be improved.

Beyond the fact that lambda conquers all, what will always stick with me is Bob’s advice to develop a point of view: I always try to start a project by articulating exactly why it’s worthwhile, and keep this perspective close at hand even when I’m deep in the technical details.

About Harper structuring his lectures as a story:

With Bob, the story is paramount. In my undergraduate days, he was well-known among the students for his bombastic and mind-expanding lectures. As his teaching assistant and then doctoral student, I saw he was forever looking for ways to improve them, to drill down to the essence. Each year he’d reconstruct and reinvent his lesson plans, and in our weekly meetings he’d often take me on a tour through his latest perspective. When we sat down to plan out a paper, the first questions were the story-theoretical: what would be the hook? What was the climax? We didn’t always agree at first what the story ought to be, but Bob impressed upon me the importance of working through it together, of putting in the effort to hammer out something that satisfied us both

Checkout:

Kern, C. and Greenstreet, M.R., 1999. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2), pp.123-193.

Formal verification, in contrast to testing, uses rigorous mathematical reasoning to show that a design meets all or parts of its specification. This requires the existence of formal descriptions for both the specification and implementa- tion. Such descriptions are given in notational frameworks with a formal semantics that unambiguously associates a mathematical object with each description, permitting these objects to be manipulated in a formal mathematical framework. […] notational frameworks, including predicate logic, temporal logic

Guo, X., Dutta, R.G., Mishra, P. and Jin, Y., 2016, May. Scalable SoC trust verification using integrated theorem proving and model checking. In 2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST) (pp. 124-129). IEEE.

Refs to look at:

Herklotz, Y., Pollard, J.D., Ramanathan, N. and Wickerson, J., 2021. Formal verification of high-level synthesis. Proceedings of the ACM on Programming Languages, 5(OOPSLA), pp.1-30.

Source code available at: https://github.com/ymherklotz/vericert

Extended compcert to make an HDL with a verilog backend.

the object of the proof is the same as the implementation of the tool.

Joyce, J.J., Liu, E., Rushby, J.M., Shankar, N., Suaya, R. and von Henke, F.W., 1990. From formal verification to silicon compilation. University of British Columbia, Department of Computer Science.

Our main conclusion is that the most effective use of formal hardware verification will be at the higher levels of VLSI system design, with lower levels best handled by conventional VLSI CAD tools.

Formal verification, the mathematical demonstration of consistency between a specification and a design

Formal hardware verification is no more than an academic exercise unless verified designs can be turned into functional chips.

Minsky, Y. and Weeks, S., 2008. Caml trading - Experiences with functional programming on Wall Street. Journal of Functional Programming, 18(4), pp.553-564.

The main point of code review is for the reader to put together an informal proof that the code they are reading does the right thing. Constructing such a proof is of course difficult, and we try to write our code to pack as much of the proof into the type system as possible.

make illegal states unrepresentable

Johnsson, T., 1985. Lambda lifting: Transforming programs to recursive equations (pp. 190-203). Springer Berlin Heidelberg.

let f x = x * x in f

ie, (λf => f) (λx => x*x)

The process of flattening out a program involving local function definitions, possibly with free variables, into a program consisting only of global function definitions, we call lambda lifting.

η-expand with each free variable in e for λx.e

Eg:

λx.y

Here, y is free. So we η-expand with y:

(λy. λx. y) y

Thus the 'inner' term is closed. All abstractions are now in the beginning.

2 rewrite rules:

let x = e1 in e2      ↔   (λx.e2) e1

letrec x = e1 in e2   ↔   let x = Y(λx.e1) in e2
                          (λx.e2) [Y(λx.e1)]

—

Attempt 1 method

Example:

let i = 5 in
letrec f = λx.f i in
f i

Converting the letrec to let,

let i = 5 in
let f = Y (λf. λx.f i) in
f i

Rewriting the inner let,

let i = 5 in
(λf. f i) [Y (λf. λx.f i)]

Rewriting the remaining let,

(λi. {(λf. f i) [Y (λf. λx.f i)]}) 5

η-expanding few subterms to make free variables bound:
 - (λf. f i)       ↔  (λi.λf.f i) i 
 - (λf. λx.f i)    ↔  (λi.λf. λx.f i) i

which makes the term:

(λi. {[(λi.λf.f i) i] [Y ((λi.λf. λx.f i) i)]}) 5

—

Attempt 2 method

Moggi, E., 1991. Notions of computation and monads. Information and computation, 93(1), pp.55-92.

A 'more refined' follow up to his 1988 paper.

—

A digression:

bind (return a) fab ≡ fab a return a >>= fab ≡ fab a

where:

ma >>= return

Monad composition operator (aka Kleisli operator) in haskell:

>=> :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) ab bc = \a -> (ab a) >>= bc

May

Maurer, L., Downen, P., Ariola, Z.M. and Peyton Jones, S., 2017, June. Compiling without continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 482-494).

—

if (if e1 then e2 else e3) then e4 else e5

becomes

if e1 then (if e2 then e4 else e5)
      else (if e3 then e4 else e5)

Links:

Functional pearl: Monadic parsing in Haskell - Graham Hutton, Erik Meijer (1998)

April

Harper, R., 1999. Proof-directed debugging. Journal of functional programming, 9(4), pp.463-469.

Partial derivatives of regular expressions and finite automaton constructions - Valentin Antimirov

Glushkov [14]: regex to NFA algorithm

https://gist.github.com/neel-krishnaswami/7353772 http://semantic-domain.blogspot.com/2013/11/antimirov-derivatives-for-regular.html

Owens, S., Reppy, J. and Turon, A., 2009. Regular-expression derivatives re-examined. Journal of Functional Programming, 19(2), pp.173-190.

Danvy, O. and Nielsen, L.R., 2001, September. Defunctionalization at work. In Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming (pp. 162-174)

Continuations: Functional representation of control

Aim: Make higher order functions first order.

Higher order function: Function that accepts another function as argument.

Whole program available => We can defunctionalize.

—

Defunctionalization example:

fun aux f = (f 1) + (f 10)

fun main x y b =
  (aux (λz. x + z)) * (aux (λz. if b then x+y else x-y))

aux is a higher order function. ∵ it takes f which itself is a function, as an argument.

Let's defunctionalize aux.

Observe the ways in which aux has been used. There are only two ways:

Let's make it a type:

datatype auxType
  = Plus of int
  | Cond of bool * int

Now we need a way to use this type to get the same effect as the original aux function.

Each of the aux usage accepts an integer as an argument. So,

(* apply : auxType -> int -> int *)
fun apply f z =
  case f of
    Plus x -> x + z
  | Cond b y -> if b then y+z else y-z

Now to have the aux and main equivalent:

(* auxDef : auxType -> int *)
fun auxDef f = (apply f 1) + (apply f 10)

main : auxType -> int -> int -> bool -> int
fun main x y b
  = (auxDef (Plus x)) * (auxDef (Cond b y))

A coq version:

Definition aux (f:nat->nat) : nat := (f 1) + (f 10).         
Definition main (x y:nat) (b:bool) : nat :=                  
  (aux (fun z=>x+z)) * (aux (fun z=>if b then y+z else y-z)).
Compute main 3 5 true.    (* 357:nat *)                      
Compute main 3 5 false.   (* 68:nat *)                       
(*Compute 17 * 21.*)                                         

(**********************************************)                                                             

Inductive auxType : Set :=                                   
| Plus: nat -> auxType                                       
| Cond: bool -> nat -> auxType.                              

Definition apply (f:auxType) (z:nat) : nat :=                
  match f with                                               
  | Plus x => x + z                                          
  | Cond b y => if b then y+z else y-z                       
  end.                                                       
Definition auxDef (f:auxType) : nat :=                       
  (apply f 1) + (apply f 10).                                
Definition mainDef (x y:nat) (b:bool) : nat :=               
  (auxDef (Plus 3)) * (auxDef (Cond b 5)).                   
Compute mainDef 3 5 true.   (* 357:nat *)                    
Compute mainDef 3 5 false.  (* 68:nat *)

— 0ⁿ1ⁿ example

sml version:

(* walk : int list -> (int list -> bool) -> bool *)
fun walk (0::xs, k)
    = walk (xs, fn (1::ys) => k ys
                 | _       => false)
  | walk (xs, k) =  k xs
  (* Base case: xs == nil *)
  (* Father... Is it over..? No king rules forever son.. *)

(* go : int list -> bool *)
fun go xs = walk (xs, fn l => l = nil)
(* go [1,2,3]; *)
(* val it = false : bool *)
(* - go [0,0,0,1,1,1]; *)
(* val it = true : bool *)

(* *)
(* Function as argument => [fn] usages. *)
(* So there are two of them. *)
(* *)

(*************************************)
(*     Defunctionalized version      *)
(*************************************)

datatype kont
  = KId
  | KWalk of kont

(* apply: kont * int list -> bool *)
fun apply (KId, xs)        = xs=nil
  | apply (KWalk k, 1::xs) = apply (k, xs)
  | apply (KWalk _, _)     = false

(* walkDef : int list -> kont -> bool *)
fun walkDef (0::xs) k = walkDef xs (KWalk k)
  | walkDef xs k = apply (k, xs)

fun goDef xs = walkDef xs KId
(* - goDef [0,0,1,1]; *)
(* val it = true : bool *)
(* - goDef [0,0,1]; *)
(* val it = false : bool *)


(********* Peano arithmetic **************************************)

(* apply: int * int list -> bool *)
fun applyP (0, xs)        = xs=nil
  | applyP (k, 1::xs) = applyP (k-1, xs)
  | applyP _     = false

(* walkDef : int list -> int -> bool *)
fun walkDefP (0::xs) k = walkDefP xs (k+1)
  | walkDefP xs k = applyP (k, xs)

fun goDefP xs = walkDefP xs 0
(* - goDefP [1,1,0]; *)
(* val it = false : bool *)
(* - goDefP [0,0,1,1]; *)
(* val it = true : bool *)
(* - goDefP [0,0,0,1,1,1]; *)
(* val it = true : bool *)

Coq version:

Require Import List.                                           
Import ListNotations.                                          

Definition isnil {A:Type} (l:list A) : bool :=                 
  match l with                                                 
  | nil => true                                                
  | _ => false                                                 
  end.                                                         

Module goHof.
  Fixpoint walk (l:list nat) (k:list nat -> bool) : bool :=
    match l with                                                 
    | 0::xs => walk xs                                           
        (fun xs => match xs with                                 
                   | 1 :: xs => k xs                             
                   | _ => false                                  
                   end)                                          
    | _ => k l                                                   
    end.                                                         
  Definition go (l:list nat) : bool := walk l (fun xs=>isnil xs).
  Compute go [0;0;1;1].                                          
  Compute go [0;0;1].                                            
End goHof.

Module goDefun.                                          
  Inductive kont : Set :=                                
  | KId: kont                                            
  | KWalk: kont -> kont.                                 

  Fixpoint apply (k:kont) (l:list nat) : bool :=         
    match k with                                         
    | KId => isnil l                                     
    | KWalk kk =>                                        
        match l with                                     
        | 1::xs => apply kk xs                           
        | _ => false                                     
        end                                              
    end.                                                 

  Fixpoint walkDef (l:list nat) (k:kont) : bool :=       
    match l with                                         
    | 0::xs => walkDef xs (KWalk k)                      
    | _ => apply k l                                     
    end.                                                 
  Definition goDef (l:list nat) : bool := walkDef l KId. 
  Compute goDef [0;0;1;1].                               
  Compute goDef [0;0;1].                                 
End goDefun.                                             

Module goDefunPeano.                                   
  Fixpoint apply (k:nat) (l:list nat) : bool :=        
    match k with                                       
    | O => isnil l                                     
    | S kk =>                                          
        match l with                                   
        | 1::xs => apply kk xs                         
        | _ => false                                   
        end                                            
    end.                                               

  Fixpoint walkDef (l:list nat) (k:nat) : bool :=      
    match l with                                       
    | 0::xs => walkDef xs (S k)                        
    | _ => apply k l                                   
    end.                                               
  Definition goDef (l:list nat) : bool := walkDef l O. 
  Compute goDef [0;0;1;1].                             
  Compute goDef [0;0;1].                               
End goDefunPeano.

—

March

Moggi, E., 1988. Computational lambda-calculus and monads. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science.

Paper that inspired use of monads in Haskell.

Physics, Topology, Logic and Computation: A Rosetta Stone - John C. Baez, Mike Stay

In Physics,

Search is still on to have a 'unified' theory.

Category Logic Computation Physics Topology
Object Proposition Type System Manifold
Morphism Proof Program? Process Cobordism

Linear operators as diagrams in quantum field theory: Feynman diagrams

\   /
 \ /
  +
  ⟆
  ⟆
  +
 / \
/   \

New stuff:

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq - Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic https://github.com/vellvm/ctrees

Choice tree Builds over Interaction trees.

The key idea is to update Xia, et al.’s interaction trees (ITrees) framework [Xia et al. 2020] with native support for nondeterminisic “choice nodes” that represent internal choices made during computation.

How "deep" the embedding is affects the amount of effort needed to implement a formal semantics - "shallower" embeddings typically allow more re-use of metalanguage features, e.g., meta-level function application can obviate the need to define and prove properties about a substitution operation; "deeper" embeddings can side-step meta-level limitations (such as Coq’s insistence on pure, total functions) at the cost of additional work to define the semantics.

to use QuickChick, one must be able to extract an executable interpreter from the semantics

In ITree monad, eutt: Equivalence up-to taus:

Inductive ctree E res
| Ret: res -> ctree E res
| Vis: ctree E res
| Later: ctree E res -> ctree E res.

Dbts:

Effect type: E A where A is the type of the 'answer' given to the system.

Brzozowski: regex to dfa

regex derivative

http://strictlypositive.org/CJ.pdf

Feb

An article. Formal Proof—Getting Started by Freek Wiedijk

Kleene Algebra with Tests and the Static Analysis of Programs: Kozen, Dexter https://hdl.handle.net/1813/5627

The automaton can be used for runtime enforcement of the security policy as well as specification. The program code is instrumented to call the automaton before all critical operations (ones that could change state of the automaton)

A. Kennedy. Compiling with continuations, continued. In Proceedings of the International Conference on Functional Programming, pages 177–190, New York, NY, USA, 2007. ACM.

'monadic terms can be translated into CPS in linear-time'

Continuation-Passing to Direct Style: Typed and Tight

CPS:

K. Farvardin and J. Reppy. From folklore to fact: Comparing implementations of stacks and continuations. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, page 75–90, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450376136. doi: 10.1145/3385412.3385994. URL https://doi.org/10.1145/3385412.3385994. 12 M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of

Beckett, R., Greenberg, M. and Walker, D., 2016, June. Temporal netkat. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 386-401).

TODO: Conversion of past-LTL to LTL

Past-LTL:

Greenberg, M., Beckett, R. and Campbell, E., 2022, June. Kleene algebra modulo theories: a framework for concrete KATs. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 594-608).

KAT consists:

assert i<50
while i<100:
    i += 1
    j += 2
assert j>100

If:

Predicates Actions
α: i<50 p: i+=1
β: i<100 q: j+=2
γ: j>100

then in KAT, this is:

α⋅(β⋅p⋅q)*⋅¬β⋅γ

One step of unrolling of this gives:

   α⋅¬β⋅γ + α⋅β⋅p⋅q⋅(β⋅p⋅q)*⋅¬β⋅γ
≡  α⋅(1 + β⋅p⋅q⋅(β⋅p⋅q)*)⋅¬β⋅γ

KMT for nat based on above example:

       V      (variables)
σ: V → ℕ      (program state. ie, env)

         t    (trace of states)
act: σ → σ

pred: σ → ℙ

KMT for 𝔹:

Refs to look at:

Handbook of theoretical computer science - Volume B: Lambda calculus chapter

Reduction of terms done using rewrite rules. No more reductions possible => normal form. Normal form => output

Church-Rosser property: normal form obtained is independent of order of evaluation of subterms.

SKI calculus:

I := λx. x
K := λx y. x
S := λx y z. x z (y z)

Harrison, W.L., Hathhorn, C. and Allwein, G., 2021, September. A Mechanized Semantic Metalanguage for High Level Synthesis. In 23rd International Symposium on Principles and Practice of Declarative Programming (pp. 1-14).

Jan

Oliveira, B.C. and Cook, W.R., 2012, September. Functional programming with structured graphs. In Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (pp. 77-88).

Code: https://github.com/michaelt/structured-graphs

PHOAS: By necessitating that the universally quantified a be kept abstract, we ensure that only names bound with a PAbs can be used in a PVar.

Generic graph:

data GraphP f a = Var a                        -- ^ Variable
                | Mu ([a] -> [f (GraphP f a)]) -- ^ Multi-binder. 'Multi-forks'
                | In (f (GraphP f a))          -- ^ Recursive step

newtype Graph = Hide {
  reveal :: forall a. GraphP f a
}

where f is a type.

(I guess Mu is ([a] -> [f (GraphP f a)]) instead of ([a] -> [(GraphP f a)]) to avoid empty looping.)

—

Application to grammars.

data Re a = Cat (Re a) (Re a)   -- ^ Seq
          | Split (Re a) (Re a) -- ^ Alt
          | Acc                 -- ^ Accept
          | Match               -- ^ Accept
          | Loop                -- ^ Recurse

Parravicini, D., Conficconi, D., Sozzo, E.D., Pilato, C. and Santambrogio, M.D., 2021. Cicero: A domain-specific architecture for efficient regular expression matching. ACM Transactions on Embedded Computing Systems (TECS), 20(5s), pp.1-24.

—

Despite significant algorithmic improvements, software solutions cannot keep pace with the increasing size of the processed data (either input strings or REs). For this reason, hardware ac- celeration is a valid alternative for computationally-intensive kernels such as those for RE matching

Hardware is better at RE matching?

— CICERO instructions

CICERO instructions are stateless

Kind Instr Meaning
Match MatchAny .
Match(c) c
NoMatch(c) [^c]
Control Split d
Jmp d
Accept AcceptPartial Match when word needn't be over
Accept Match when word over

— CICERO compiler

— Single char mechanism example:

No Instr
1 Match a
2 Match b
3 Split 7
4 Match a
5 Match b
6 Jmp 10
7 Match b
8 Match b
9 Jmp 10
10 Acceptpartial
FIFO-0 FIFO-1 Parsed
Match a
Match b a

Comment:

—

Baaij, C., Kooijman, M., Kuper, J., Boeijink, A. and Gerards, M., 2010, September. Cλash: Structural descriptions of synchronous hardware using haskell. In 2010 13th Euromicro Conference on Digital System Design: Architectures, Methods and Tools (pp. 714-721). IEEE.

Possible mapping to hardware:

Eg:

-- res = a*b + c
mac a b c = add (mul a b) c
      +--------------------------+
      |   +-----+       +-----+  |
a ----|---|     |-------| add |  |
b ----|---| mul |    +--|     |--|--->
      |   +-----+    |  +-----+  |
c ----|--------------+           |
      +--------------------------+

—

Choices:

—

Not all of Haskell’s typing constructs have a clear translation to hardware

TODO: An example of a construct that can't be translated to hardware?

—

Type annotation:

VHDL Clash
Entity Type annotation
Mandatory Can often be inferred

— Built-in types:

User-defined datatypes with multiple constructors where at least one constructor accepts an argument is not supported.

TODO: Try:

data Eg = One Int
        | Two
        deriving Show

Works but I guess won't synthesize.

> :{
| data Eg = One Int
|         | Two
|         deriving Show
| :}
> One 2
One 2

—

Advantages of clash as HDL:

Ad-hoc polymorphism:

Top level (topEntity) cannot be left polymorphic and must have a concrete type. Only the design is polymorphic.

Higher order functions:

Eg: negVector v = map not v

— Todo:

Harper, R., Duba, B.F. and MacQueen, D., 1993. Typing first-class continuations in ML. Journal of functional programming, 3(4), pp.465-484.

Continuations:

callcc:

throw:

Milner-style soundness theorem: 'Well-typed programs cannot go wrong'

Oliveira, B.C. and Cook, W.R., 2012, September. Functional programming with structured graphs. In Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (pp. 77-88).

Pnueli, A. and Zaks, 2006. A., PSL Model Checking and Run-time Verification via Testers Technical Report: TR2006-881. Notations used:

Boolean semantics (⊫):

∀(p ∈ P) (b b₁ b₂ ∈ 𝔹) then,

  1. l ⊫ p iff p ∈ l
  2. l ⊫ ¬b iff l ⊯ b
  3. l ⊫ true , l ⊯ false
  4. l ⊫ b₁ ∧ b₂ iff l ⊫ b₁ and l ⊫ b₂

—

(Unclocked) SERE semantics (⫢):

∀ (r r₁ r₂ : Unclocked SERE)

Meaning
v ⫢ {r} ↔︎ v ⫢ r just the bracket for grouping
v ⫢ b ↔︎ │v│=1 ∧ v[0] ⊫ b
v ⫢ r₁;r₂ ↔︎
v ⫢ r₁:r₂ ↔︎
v ⫢ r₁│r₂ ↔︎
v ⫢ r₁ && r₂ ↔︎
v ⫢ [*0] ↔︎ v = ε

—

FL = Foundation language

FL Formula semantics (⊨):

—

Theorem 1. For every SERE r of length n, there exists an associated grammar G with the number of productions O(2n). If we restrict SERE’s to the three traditional operators: concatenation ( ; ), union ( | ), and Kleene closure ( [∗] ), the number of productions becomes linear in the size of r.

Sheon Han, 2022. How to Write Software With Mathematical Perfection. Quanta Magazine

Lamport laments how programmers often cobble together a system before writing a proper specification, whereas chefs would never cater a banquet without first knowing that their recipes will work.

In the 1970s, when people were reasoning about programs, they were proving properties of the program itself stated in terms of programming languages. Then people realized that they should really be stating what the program is supposed to accomplish first — the program’s behaviors.

one practical method of writing these higher-level specifications for concurrent systems was writing them as abstract algorithms. With TLA+, I was able to express them mathematically in a completely rigorous fashion. And everything clicked. What that involves is basically not trying to write algorithms in a programming language: If you really want to do things right, you need to write your algorithm in the terms of mathematics.

The importance of thinking and writing before you code needs to be taught in undergraduate computer science courses

True, most of the code written by programmers across the world doesn’t require very precise statements about what it’s supposed to do. But there are things that are important and need to be correct. … For the kind of application where precision is important, you need to be very rigorous.

Model checking is a method for exhaustively testing all executions of a small model of the system. It just shows the correctness of the model, not of the algorithm. … In practice, model checking checks all executions of a small instance of the algorithm. And if you’re lucky, you can check large enough instances that it gives you enough confidence in the algorithm. But the proof can prove its correctness for a system of any size and for any use of the algorithm.

Thompson, K., 1968. Programming techniques: Regular expression search algorithm. Communications of the ACM, 11(6), pp.419-422.

Operations:

a(b│c)*d Input
a.(b│c)*.d With explicit concat
abc│*.d. Postfix form

2022

Automata-Based Assertion-Checker Synthesis of PSL Properties - Marc Boulé and Zeljko Zilic Runtime Verification for LTL and TLTL - Andreas Bauer, Martin Leucker, Christian Schallhart

Dec

Manna, Z. and Pnueli, A., 1991. Completing the temporal picture. Theoretical Computer Science, 83(1), pp.97-130.

Pnueli, A. and Arons, T., 2003. Tlpvs: A pvs-based ltl verification system. In Verification: Theory and Practice (pp. 598-625). Springer, Berlin, Heidelberg.

tlpvs: https://cs.nyu.edu/acsys/tlpvs/tlpvs.html

—

The advantage of using this system [TLPVS] over using a general theorem prover is that the included rules and strategies free the user from much of the drudge work.

—

About using an existing theorem prover:

In so doing we enable the user to benefit from the abilities of a well developed theorem prover, with a large community of users who continuously develop and improve the prover’s power. Basing our system on pvs, and making the theories available, makes it extremely flexible. When necessary users are able to modify or extend the framework to fit their own needs; they are not restricted by the existing set of proof rules and strategies.

—

ref: [4] (STeP)

Boulé, M. and Zilic, Z., 2006, November. Efficient automata-based assertion-checker synthesis of PSL properties. In 2006 IEEE International High Level Design Validation and Test Workshop (pp. 69-76). IEEE.

—

PSL expressions will be implicitly clocked to the default clock, specified with PSL's default clock directive.

DBT: What's the clock directive?

—

Some forms of properties are not suitable for simulation and can only be evaluated by formal methods. The portion of PSL suitable for simulation is referred to as the simple subset of PSL.

Leucker, M. and Schallhart, C., 2009. A brief account of runtime verification. The journal of logic and algebraic programming, 78(5), pp.293-303.

3 ways:

MC ITP Testing
Rigorous Rigorous Not rigorous
Not scalable Scalable Scalable
Formal Formal Informal
Automatic Manual Automatic
Ony finite syst Infinite syst as well Infinite syst as well
MC RV
Infinite trace examined Finite trace examined

Furthermore, model checking suffers from the so-called state explosion problem, which terms the fact that analyzing all executions of a system is typically been carried out by generating the whole state space of the underlying system, which is often huge. Considering a single run, on the other hand, does usually not yield any memory problems, provided that when monitoring online only a finite history of the execution has to be stored.

RV vs Testing:

Nevertheless, the implementation might behave slightly different than predicted by the model. Runtime verification may then be used to easily check the actual execution of the system, to make sure that the implementation really meets its correctness properties. Thus, runtime verification may act as a partner to theorem proving and model checking.

DBT: μ-calculus?

Ref: [43], [9]/[11]

Hunt Jr, W.A., Kaufmann, M., Moore, J.S. and Slobodova, A., 2017. Industrial hardware and software verification with ACL2. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375(2104), p.20150399.

The attractiveness of using theorem provers for system design verification lies in their generality

DBT: How can Skolem constants simply acquire the place of a (universally) quantified variable?

—

The microprocessor verification problem is to show that the traces induced by the implementation transition system are a subset of the traces induced by the specification transition system, where subset has to be carefully defined by use of an abstraction mapping.

Kind of resonates with runtime verification..

—

Schneider, K. and Kropf, T., 1995. Verifying hardware correctness by combining theorem proving and model checking. Higher Order Logic Theorem Proving and Its Applications: Short Presentations, 89, p.104.

Beyer, S., Jacobi, C., Kroening, D. and Leinenbach, D., 2002. Correct hardware by synthesis from PVS. Submitted for publication.

DBT: I wonder why this was so?

While model checking is a good way to verify control dominated designs, the verification of combinatorially complex designs such as floating point units is currently beyond the scope of model-checkers

Shankar, N., 1996, November. PVS: Combining specification, proof checking, and model checking. In International Conference on Formal Methods in Computer-Aided Design (pp. 257-264). Springer, Berlin, Heidelberg.

—-

| bilinear and     | Ⓧ | Multiplicatives |
| bilinear or      | ⅋ |                 |
| bilinear implies | ⊸ |                 |
|------------------+---+-----------------|
| linear or        | ⊕ | Additives       |
| linear and       | & |                 |
|------------------+---+-----------------|
| □                | ! | Exponentials    |
| ◇                | ? |                 |

Ishio, C. and Asai, K., 2022, November. Type System for Four Delimited Control Operators. In Proceedings of the 21st ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (pp. 45-58).

An example expression involving shift/reset. Shift is S and reset is the <>.

  <(Sk. k (k 2)) + 3> + 4
= <k (k 2) [λx. <x+3> / k]> + 4
= (λx. <x + 3>) ((λx. <x + 3>) 2) + 4
= [(λx. <x + 3>) 5] + 4
= 8 + 4
= 12

  <(Fk1. (2+k1 1)) + Fk2. (4+k2 3)>
= <(2+k1 1)[(λx. x + Fk2. (4+k2 3)) / k1]>
= <(2+(λx. x + Fk2. (4+k2 3)) 1)>
= <(2+ (1 + Fk2. (4+k2 3))>
= <(4+k2 3)[ (λx. 2 + (1 + x)) / k2 ]>
= <(4+(λx. 2 + (1 + x)) 3)>
= <(4+(2 + (1 + 3)))>
= 10

  <<(S0k1. S0k2. e) + 2> + 3>
=

Nov

Oct

CoInductive ITree 
(* Halt. Leaf *)
| Ret: ITree

(* Visible stuff. One child node *)
| Tau: ITree -> ITree

(* Internal stuff. Two children node *)
| Vis:

Continuation tree. Free monad

A reminder of monadic laws:

x <- ret v ;; k x ≡ k v
x <- t ;; ret x ≡ t
(x <- (y <- s ;; t) ;; u) ≡ (y <- s ;; x <- t ;; u)

itree E R

E: Type -> Type is the type of external interactions.

CoInductive itree (E:Type -> Type) (R:Type) : Type :=
| Ret (r:R) : itree E R                    (* Done. Result is [r] *)
| Tau (t:itree E R) : itree E R            (* Keep going with [t] *)
| Vis: forall {A:Type} (e:E A),
    (A -> itree E R) -> itree E R
  (* Got a result, gave back an answer of type [A]
     from where the continuation resumes computation *)

—

Example:

(*            answer type
                 ^
                 |
                 |        *)
Inductive IO : Type -> Type :=
| Input: IO nat
| Output: nat -> IO unit.

Input: expects nothing as input, but wants nat as output Output: expects nat as input, but wants nothing (unit) as output

A program that keeps reading input and echoing it:

CoFixpoint echo : itree IO void :=
  Vis Input (fun x =>
    Vis (Output x) (fun _ => echo)).

void is notation from Empty_set from Coq.Ensembles. It has no constructor, making it impossible for us to make a value of that type.

Another example: An infinite loop:

CoFixpoint spin: itree IO void := Tau spin.
(* The value of [E], which is in this case [IO], is irrelevant in this I guess.. *)

The above two examples never halt. Here's an example that halts when input is 9:

CoFixpoint kill9: itree IO unit :=
  Vis Input (fun x:nat =>
    if Nat.eqb x 9 then (Ret tt)
    else kill9).

This program doesn't give out 'output'. If we wanted some kind of output as well, I suppose we can do:

CoFixpoint kill9': itree IO unit :=
  Vis Input (fun x:nat =>
    if Nat.eqb x 9 then (Ret tt)
    else (Vis (Output x) (fun _ => kill9')).

Notations:

(* Empty type. Like [False], but in [Type]. *)
Inductive void : Type :=.

(* Interactive tree type *)
CoInductive itree {E:Type -> Type} {R:Type}: Type :=
| Ret: R -> itree
| Tau: itree -> itree
| Vis: forall {A:Type},
    E A -> (A -> itree) -> itree.
Arguments itree : clear implicits.

(* Env interaction type *)
(*           Answer/response type
                |                    *)
Inductive IO: Type -> Type :=
| Input: IO nat
| Output: nat -> IO unit.

(* Idle infinite loop *)
CoFixpoint spin: itree IO void := Tau spin.

(* Echo infinite loop *)
CoFixpoint echo: itree IO void :=
  Vis Input (fun n:nat =>
    Vis (Output n) (fun _:unit => echo)).

(* Halt when input is 9 while spinning otherwise *)
CoFixpoint kill9: itree IO unit :=
  Vis Input (fun n:nat =>
    if Nat.eqb n 9 then Ret tt
    else kill9).

(* Halt when input is 9 while echoing otherwise *)
CoFixpoint kill9out: itree IO unit :=
  Vis Input (fun n:nat =>
    if Nat.eqb n 9 then Ret tt

These are just the interaction tree. We define handler function to give semantics to itree values.

Effects => external events E. A monad.

— Todo:

Doubts:

Sere A := Cat A (Sere A)
        | Alt (Sere A) (Sere A)
        | And (Sere A) (Sere A)
        | Fuse (Sere A) (Sere A)
        | Star (Sere A)

(* Property *)
Ppty A := Bool (A->𝔹)
        | Neg (A->𝔹)
        | Re (Sere A)
        | Abort (Ppty A) (A->𝔹)
        | PAnd (Ppty A) (Ppty A)
        | Impl (Sere A) (Ppty A)
        | Iff (A->𝔹) (A->𝔹)

s!: strong sequence. Should definitely be matched before the end of execution.

2021

                Quote
     +-----------------------------+
     |                             |
     ∧                             ∨
     |                             |
concrete synatx             reified syntax
     |                             |
     ∧                             ∨
     |                             |
     +-----------------------------+
              Unquote