Questions tagged [termination]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
9 votes
1 answer
172 views

Universe inconsistency as an effect

The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
  • 2,832
6 votes
1 answer
159 views

Termination and confluence -- which goes first?

I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by: the well-typedness of the clauses (type check) the coverage of the patterns (...
  • 5,424
0 votes
1 answer
57 views

Well founded recursion through lists

I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with: ...
  • 263
5 votes
1 answer
140 views

How to convince Agda that definition is terminating in the presence of unapplied recursion?

In the following, termination check fails for Df: ...
5 votes
1 answer
149 views

Strictly-monotone "max" operation for constructive Brouwer-trees?

The Setting I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e. ...