8

This is a really interesting question and only partially understood. The $ \newcommand{\OUT}[2]{\overline{#1} #2 } $ precise answer to such questions depends in subtle ways on exactly what the ambient $\pi$-calculus is and exactly what feature you are encoding. For sums you need to realise that there are different kinds of sums for example input ...


8

Principia Mathematica was a largely response to the various paradoxes discovered in mathematical logic at the turn of the 20th century. However the work itself, which has often been obliquely praised as an 'unreadable masterpiece' is somewhat clumsy and more modern foundations have been crafted. To describe most of mathematics, you have several choices: ...


8

Several points: As far as I know, Principia Mathematica uses essentially a formalization of set theory using a typed first order logic. It would therefore be tempting to use a first-order automated theorem prover like Prover 9 or possibly ACL2 to formalize your statements. However, I am seeing several set-theoretic constructions (like $\in$, $\cap, \subset$)...


5

Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding. Symbolic Execution for Software Testing: Three Decades Later, Cristian Cadar and Koushik Sen, 2013. All You Ever Wanted to Know about Dynamic Taint Analysis and ...


4

Prolog embodies the idea of computation as proof search. That is: a program is a formula which we would like to satisfy, the computation is the proof search, and the result is the witness for the formula. To make this idea work we need to reformulate the rules of first-order logic so that they can be read as instructions for execution of a proof search. We ...


3

In general, the technique used is known as "fuzzing". Not all errors are equally likely. Let's consider two hypothetical errors: System A incorrectly rejects a filename if it contains an | anywhere. System A incorrectly rejects a filename if it contains a prime number of b characters. Errors of the second type are much, much rarer, but this is not ...


2

Basically, almost any machine learning or compression method is an approximation to Kolmogorov complexity: If you have any computable probability distribution which assigns your data probability $p(x)$ then, by the Kraft inequality, you have a compressor which compresses your data in $- \log p(x)$ bits. If you have any computable compressor C which ...


2

For the concrete case of a specification of a regular language, there is the Java String Analyzer which roughly is able to compute a finite state automaton (i.e. regular expression) of the set of strings accepted by a Java method, using various techniques in static analysis. While the paper deals directly with the set of strings generated by a piece of Java ...


2

First of all, the place for this question is cs.se, not here. But since I've already written an answer, I'll leave it. There is a formal definition of computability: a function $f$ is computable if there is a Turing machine that, given input $x$, always halts with $f(x)$ written on its tape. You could of course define more general computability, which uses ...


1

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question. [1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147


1

Some of the performance-related things you can objectively compare between different databases: IO complexity and computational complexity of different queries. E.g. there are different ways to do joins, sorting, different kinds of indices (including "no indices"), with objectively different asymptotic complexity. There are also column-oriented and row-...


1

Prolog deals with a formal system which is a small fragment of first order logic: it uses a logic of definite clauses, which are disjunctions of atoms and negated atoms, with the resolution rule as only inference rule. If you're not completely familiar to formal (logic) systems you just need to know that they are basically sets of rules: rules that ...


1

Being a beginner to Symbolic Execution (SE) myself, I would suggest: Symbolic execution and program testing: this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation. All you ever wanted to know...: this paper surveys SE and its applications to Security. The third step may be to ...


1

I don't think this question is related at all with approximation algorithms, or theoretical CS. Please take the following as some free, non-exhaustive, thoughts on your question. It seems to me that what you want is just the probability that a given sequence of words contains only valid words. Let me assume that each word is chosen independently (which it ...


1

There were a lot of publication on extending and or formalizing RBAC/SOD with LTL or other flavors of temporal logics, not sure of other AC models. Google Scholar (or simple google) search with yield a bunch of articles. Most of them might be not sufficiently formal for somebody like yourself, yet might be of some interest. Not sure is LTL the best way. Yet ...


Only top voted, non community-wiki answers of a minimum length are eligible