Questions tagged [terminology]

For questions about words, phrases and definitions that are specific to proof assistants.

Filter by
Sorted by
Tagged with
2 votes
0 answers
74 views

Formally verified email or communication?

This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway. I would like to consider the simplest possible formally verified ...
Julius H.'s user avatar
  • 175
3 votes
1 answer
129 views

What's the difference between a computation rule and a definitional equality?

In http://www.cse.chalmers.se/~coquand/comp.pdf, Coquand said: One important point is that we cannot hope this computation rule to be interpreted as a definitional equality, since reflexivity is not ...
ice1000's user avatar
  • 5,857
5 votes
1 answer
139 views

What is a 'truncation'?

I've heard of many truncations in homotopy type theory, like propositional truncation, homotopy n-truncation, etc., and I think I understand these specific concepts. People also talk about 'double-...
ice1000's user avatar
  • 5,857
3 votes
1 answer
124 views

Difference between implementation and formalisation in a proof assistant

Some authors refer to their works as "implementation of the theory in (let's say) Agda", some refer as "formalization of the theory in Agda". What is the difference between them?
phdstudent's user avatar
5 votes
1 answer
297 views

What is a weak function space and what does it have to do with HOAS?

What is a weak function space and what does it have to do with higher order abstract syntax? I mean I know what a weak function space is. It's that thing you use for HOAS in Lambda Prolog or toolkits ...
Molly Stewart-Gallus's user avatar
6 votes
2 answers
210 views

Does ST$\lambda$C equal to simple type theory?

Is "simple type theory" a folklore, or does it have a formal definition? On nlab, it's only discussed "practically": In practice any type theory is called a simple type theory if ...
ice1000's user avatar
  • 5,857
7 votes
0 answers
89 views

What is focusing and how do I use it?

I have heard the term "focusing" with respect to the sequent calculus (System LK) and related calculi like the $\bar{\lambda} \mu \tilde{\mu}$-calculus. What is focusing and how do I use it? ...
Molly Stewart-Gallus's user avatar
10 votes
2 answers
149 views

What's "predicative" about pC(u)IC?

Timany and Sozeau's Predicative Calculus of Cumulative Inductive Constructions (pCuIC) [1] adds extra cumulativity to the inductive types of (Lee and Werner's [2], I think?) pCIC. But what does the &...
ionchy's user avatar
  • 906
13 votes
2 answers
522 views

What is a commuting conversion and why are they problematic?

Off and on I have heard of the jargon "commuting conversion" but I don't really know what it means. I've heard commuting conversions are problematic but I don't know why.
Molly Stewart-Gallus's user avatar
10 votes
0 answers
313 views

What's "Swedish" style of doing type theory or proof assistants?

Jon Sterling said Conor McBride's universe polymorphism proposal to be: seems to have worked well in Swedish experiments I wonder, what does "Swedish" mean here? What kind of type theory ...
ice1000's user avatar
  • 5,857
29 votes
1 answer
1k views

What is an algebraic data type?

When I first learned Haskell, I was told that you use data keyword to define an "algebraic data type", or a "sum type". Then I learned the idea ...
ice1000's user avatar
  • 5,857
9 votes
1 answer
118 views

How did the meaning of "lifting" in proof assistants arise?

In topology, the notion of "lifting" has a quite a long history, starting with the theory of covering spaces, where the classic example is that if you take an outdoor spiral staircase, $S$ ...
John's user avatar
  • 325
3 votes
1 answer
179 views

What is an eliminator?

What is an eliminator? Are there any differences between an eliminator and an elimination form (such as $\pi_1$ and $\pi_2$ for binary products)? Does every type have exactly one? Is the type of the ...
Greg Nisbet's user avatar
  • 2,711
18 votes
3 answers
791 views

What is a Proof Assistant?

How would you explain to a beginner in simple terms, what a Proof Assistant is?
taylor.2317's user avatar
  • 1,308