Skip to main content
Share Your Experience: Take the 2024 Developer Survey
13 votes

Why/when do we ever need transfinite loop variants?

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 ...
Andrej Bauer's user avatar
  • 29.1k
12 votes

Formal semantics of OCaml in Coq

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 ...
Neel Krishnaswami's user avatar
9 votes
Accepted

Why is it impossible to prove software to be correct?

Whatever you heard is false. Proving programs correct is not only possible, it is also done in practice on large scale. There is an entire branch of computer science, namely formal methods which ...
Andrej Bauer's user avatar
  • 29.1k
9 votes

Why/when do we ever need transfinite loop variants?

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 ...
Henning Basold's user avatar
8 votes

Formal semantics of OCaml in Coq

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 ...
gasche's user avatar
  • 2,040
6 votes

Verified type checkers

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 ...
Andrej Bauer's user avatar
  • 29.1k
6 votes
Accepted

Lee's algorithm for synthesis of ranking functions in size-change termination proofs

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 ...
cody's user avatar
  • 13.9k
6 votes

How to determine whether a proof requires "higher-order reasoning techniques"?

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 ...
Cris P's user avatar
  • 161
4 votes
Accepted

Proof that the theory of rationals is convex

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 ...
Klaus Draeger's user avatar
4 votes
Accepted

Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

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 ...
cody's user avatar
  • 13.9k
4 votes

What's the difference between an invariant and an "inductive" invariant?

Just to expand on Jukka's excellent answer, the question of finding invariants usually arises when trying to establish safety properties. A safety property $S$ is a property that we wish for the ...
Motorhead's user avatar
  • 181
4 votes
Accepted

Ordering sequences containing bitvectors for size-change termination

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 ...
cody's user avatar
  • 13.9k
3 votes
Accepted

State of the Art for the Monadic Class?

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 ...
cody's user avatar
  • 13.9k
3 votes

State of the Art for the Monadic Class?

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 ...
Neel Krishnaswami's user avatar
3 votes

Why/when do we ever need transfinite loop variants?

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 ...
Dan Doel's user avatar
  • 1,021
3 votes

Nominal Tree Languages i.e. with Binders and Infinite Symbols?

I think section 3.1 (titled "Nominal tree automata") of this paper: https://drops.dagstuhl.de/opus/volltexte/2019/11434/ may be what you're looking for, they use λ-terms as their example. In ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
2 votes

How are safety/liveness languages defined on the set of finite or infinite words?

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 ...
Denis's user avatar
  • 8,893
1 vote

Why is it impossible to prove software to be correct?

I'm wondering if you've misheard or heard a distorted version of the Donald Knuth Quote: Beware of bugs in the above code; I have only proved it correct, not tried it.' There is definitely some sort ...
Joey Eremondi's user avatar

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