18

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on Page 3: Neither the compiler nor the prover need to be correct in order to be guaranteed to detect incorrect compiler output. This is a significant advantage ...


12

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer. Full completeness: "Sound and complete" is a ...


12

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a ...


12

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid invariant may require transfinite induction! For instance, we could write a loop that computes the Goodstein sequence. This is particular sequence of numbers ...


9

I would like to add the following to Andrej's response (not enough rep for a comment). Indeed, we cannot avoid ordinals but we may hide them. One approach is to use some modal logic that takes essentially care of "we're one step closer to the end" without mentioning ordinals explicitly. This approach has been used successfully by Nakano and other people to ...


8

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and properties of type inference for a ML language with (recursion and) structural polymorphism, thus formalizing one of the more advanced corners of OCaml (...


6

Here are some results of a simple Google search: Certification of a Type Inference Tool for ML: Damas–Milner within Coq by Catherine Dubois and Valérie Ménissier-Morain Formalization of a Polymorphic Subtyping Algorithm by Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers type-inference formalization in Coq, based on A Rewriting Semantics for Type ...


6

The complexity is acceptable in current verifiers, and has been implemented in at least the AProVE termination analysis tool for term rewrite systems. They describe their implementation in Lazy Abstraction for Size-Change Termination, by Codish, Fuhs, Giesl & Schneider-Kamp, basing their implementation on the papers you refer to. Performance is good ...


6

Briefly, every theorem stated in first-order logic has a first-order proof. In his book "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews develops both first-order logic and a system of higher-order logic Q0, which is generally considered to be the theory basis of modern higher-order provers. (See the introduction to the HOL logic ...


5

I don't know if it has been studied before, but after a quick look I think it should be PSPACE complete. We can build a reduction using the Nondeterministic Constraint Logic model of computation (NCL). I quick idea is the following (I assume you're familiar with the NCL model): given an NCL graph $G$, you can replace red and blue directed edges with a ...


5

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$ Details: The detailed meaning of full abstraction and full completeness depends on the nature of what/where/how you are interpreting. Here is a ...


4

Surely, you want $s_1 < s_2$ if there is a $t$ such that $s_1.t < s_2.t$ and $s_1.u \leq s_2.u$ for every other field $u$. That, at least, gives you a well-founded order. But there are many other well-founded orders on tuples, e.g. lexicographical order for some order of the fields (though you might need a heuristic to find the order), and various ...


4

Levy's call by push value calculus makes a distinction between values and their thunks. For a value v of type ty the computation thunk v has type U ty. Lindley and McBride's Frank language, inspired by CBPV, also makes this distinction between computations and values explicit, though unlike Haskell, Frank is strict.


4

If I read you correctly, the intuition you have in mind goes like this: Suppose we have a program $P$, which takes a function as an argument. Further suppose that we have two functions $f$ and $g$, such that $f$ terminates on a subset of the inputs $g$ terminates on, but agrees with $g$ whenever they both terminate. Now, if $P\;g$ is partially correct, ...


4

The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points between $p$ and $q$ are also in $S_F$. Now suppose that $F\Rightarrow G$, where $G$ is a disjunction of equations $x_1=y_1\vee\ldots\vee x_n=y_n$ (note that ...


4

As often in these matters, the encodings are important: you could have some silly encoding of Turing machines or Gallina terms or both where an input string $\langle n\rangle$ represents "the $n$-th well-typed term in Gallina". The TM that accepts this is trivial, and you'd be able to prove correctness and termination of the machine easily. See e.g. this ...


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 ...


3

I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for the Monadic Fragment and Guarded Negation Fragment. This implements what you want, though I couldn't find the implementation online.


3

I imagine that you can prove this straight from the operational semantics using the standard operational precongruence (assuming that you have a sequential language). Some of the relevant techniques have been collected in Operationally-based theories of program equivalence by Andy Pitts. If you have a Hoare logic of partial correctness for the language you ...


3

I will attempt to write the same answer as Neel with fewer technicalities (and therefore not really correct). By the way, you are using very strange terminology, which I will avoid. For each type $T$ appearing in a programming language we can define a partial order $\leq_T$ as follows: on the integers we define $p \leq_{\mathtt{int}} q$ to mean: "if $p$ ...


3

Two or three years ago I started taking a look to formal methods applied to software. This was a quest driven by curiosity, and by the feeling that I had to learn programming tools and methods with longer time-spans. Although I dreamed wishfully about a Silver Bullet, I really thought that there was not an answer to the question: "How can I write a correct ...


3

If I may add something, too, I'd suggest that some of the ways ordinals are presented tend to make them sound more 'suspicious' than they actually are. At least, I think there are other ways of presenting them that make them seem less suspicious. For instance, I think it's pretty common for people to say or imply that using transfinite ordinals involves ...


2

The answer is yes to all questions, so it is enough to answer 2 and 4, as the definitions work in particular for languages of finite words: A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is safety if whenever $u\notin P$, then $u$ has a finite prefix $u'\in\Sigma^*$ such that for any word $v$, $u'v\notin P$. A language $P\subseteq \Sigma^*\cup\Sigma^\...


2

The gist of the question is, given that quantum probability is a source of true randomness, how does that effect the extended (or efficient, or polynomial-time) Church-Turing thesis? The answer is that, per conjecture, it doesn't affect it. People conjecture that BPP = P, i.e., that randomized algorithms can be derandomized with pseudo-random-number ...


2

In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are equivalent to regular tree grammars, so most of the algorithms developed there should portable to monadic FOL as well. I don't know the area that well, but set ...


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

Your construction for bad prefixes is not correct on NBA's. For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an accepting sink if the first letter is $x$ and to a rejecting sink if the first letter is not $x$. Then the language recognized is $A^\omega$, but the set of "bad ...


1

Herlihy and Wing write on p. 477: In conclusion, the rep invariant $\mathbf{I}$ must be continually satisfied and the abstraction function continually defined, not only between abstract operations, but also between rep operations implementing abstract operations. The abstraction function maps each rep value to a nonempty set of abstract values: $$ \...


1

The powerful formalism you are looking for cannot exist, for otherwise we could solve the halting problem. Here is the sketch of an argument why. Consider Hoare triples $\{A\} P \{B\}$ for partial correctness. If we had a (computable) upper bound that related program length to the lengths of correctness proofs, then we could apply it to the assertion $$\...


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