4 ms·

CFML stands for "Characteristic Formulae for ML". Characteristic formulae are a powerful concept of program logic. Simplifying a great deal, given a program M,

by mafribe 11y ago

CFML stands for "Characteristic Formulae for ML". Characteristic formulae are a powerful concept of program logic. Simplifying a great deal, given a program M, a characteristic formula for M is a pair (A, B) of logical formula such that 1. {A} M {B}, i.e. if precondition A is satisfied, then the result of running program M satisfies postcondition B. 2. Whenever another program N satisfies {A} N {B} then M and N are contextually indistinguishable. In other words, the pair (A, B) specifies everything that can be said about M in the ambient program logic. Note that a program logic does not necessarily admit characteristic formulae for all programs. Program logics that do are 'in harmony' with the operational semantics in that the logic makes exactly the same distinctions about programs that the operational semantics makes. Characteristic formulae come the theory of communicating processes, see [1] for an overview. [1] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic.

vog 11y ago
While I appreciate your insightful comment very much, I don't see how it addresses the concern of the parent comment. (i.e. that the name "CFML" is already taken and thus may have the potential of confusion)
- mafribe 11y ago
  Most (all?) three- and four-letter abbreviations are already used. Context disambiguates.
  - vog 11y ago
    Thanks for trying, but this still seems to utterly miss the point of the parent posting. The parent posting did not merely say that "CFML" is already used in some totally unrelated context. That complaint would be indeed pointless. Rather, they noted that there is another computer language with that abbreviation. So the context of both "CFML" is very close. Or, are you saying that it is never worth worrying about naming/abbreviation clashes, because you can always trust on the disambiguation by context?
    - mafribe 11y ago
      CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of the program; (2) a Coq library, more precisely a library of Coq tactics, that enables users interactively to manipulate characteristic formulae of Caml programs in Coq. So Charguéraud's CFML is far away from cold fusion that context can always disambiguate. And if not ... is the sky going to fall down?

by mafribe 11y ago

vog 11y ago

While I appreciate your insightful comment very much, I don't see how it addresses the concern of the parent comment. (i.e. that the name "CFML" is already taken and thus may have the potential of confusion)

mafribe 11y ago
Most (all?) three- and four-letter abbreviations are already used. Context disambiguates.
- vog 11y ago
  Thanks for trying, but this still seems to utterly miss the point of the parent posting. The parent posting did not merely say that "CFML" is already used in some totally unrelated context. That complaint would be indeed pointless. Rather, they noted that there is another computer language with that abbreviation. So the context of both "CFML" is very close. Or, are you saying that it is never worth worrying about naming/abbreviation clashes, because you can always trust on the disambiguation by context?
  - mafribe 11y ago
    CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of the program; (2) a Coq library, more precisely a library of Coq tactics, that enables users interactively to manipulate characteristic formulae of Caml programs in Coq. So Charguéraud's CFML is far away from cold fusion that context can always disambiguate. And if not ... is the sky going to fall down?