<p>In the literature of refinement type systems and program logics, I've observed that many authors choose to confine the programs under consideration to A-normal form. For context, A-normal form features <code>let x = t1 in t2</code> as the sole sequencing construct, with no implicit sequencing present in any other construct.</p>
<p>I understand that every program can be transformed to an equivalent program in A-normal form. I'm curious to understand the rationale behind this common practice. Why do refinement type systems and program logics often favor A-normal form? What advantages or simplifications does this particular form bring in the context of type systems and program proofs?</p>

CC BY-SA 4.0
2024-01-30T08:24:46.690Z
Wikipedia disagrees with you about [A-nromal form](https://en.wikipedia.org/wiki/A-normal_form), but more importantly, what are these rumoured papers? Please provide at least one specific such paper so that we can pin down what you're talking about. Right now there isn't much to go on: your description of A-normal form is slightly different from the one I know, and you did not actually refer to any specific papers.
Andrej Bauer
CC BY-SA 4.0
2024-01-30T10:03:30.193Z
@andrej Thanks for the comment. Here's one paper which uses the A-normal form in the formalization of a sequential Separation logic: https://dl.acm.org/doi/abs/10.1145/3408998 c.f. last paragraph of 4.1.
yiyuan-cao
CC BY-SA 4.0
2024-01-30T10:13:29.003Z
And [this paper](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/9A47A8663CD8A7147E2F17865C368094/S0960129521000487a.pdf/two_decades_of_automatic_amortized_resource_analysis.pdf) talks about the use of A-normal form in a preprocessing step before type checking, c.f. the bottom of page 7.
yiyuan-cao
CC BY-SA 4.0
2024-02-03T16:00:45.467Z
Simplicity: the logical rules become a tiny bit simpler when the arguments to all interesting operations in the ambient language are  trivial (constants or variables). If you allow full expressions, e.g. $M + N$ instead of, e.g., $x+y$ or $2 + 7$, then the logical rules also need to cater for the evaluation of $M$ and of $M$, and for every operation.
Martin Berger
<type-theory><type-systems><proof-assistants><program-verification><program-logic>
Why use A-normal form in type systems and program verification systems?
yiyuan-cao
# Why use A-normal form in type systems and program verification systems?

(Asked by: username_0 on 2024-01-30)

In the literature of refinement type systems and program logics, I've observed that many authors choose to confine the programs under consideration to A-normal form. For context, A-normal form features `let x = t1 in t2` as the sole sequencing construct, with no implicit sequencing present in any other construct.

I understand that every program can be transformed to an equivalent program in A-normal form. I'm curious to understand the rationale behind this common practice. Why do refinement type systems and program logics often favor A-normal form? What advantages or simplifications does this particular form bring in the context of type systems and program proofs?

**Tags:** type-theory, type-systems, proof-assistants, program-verification, program-logic

> **Comments:**
> **username_1**: Wikipedia disagrees with you about [A-nromal form](https://en.wikipedia.org/wiki/A-normal_form), but more importantly, what are these rumoured papers? Please provide at least one specific such paper so that we can pin down what you're talking about. Right now there isn't much to go on: your description of A-normal form is slightly different from the one I know, and you did not actually refer to any specific papers.  
> **username_0**: @andrej Thanks for the comment. Here's one paper which uses the A-normal form in the formalization of a sequential Separation logic: https://dl.acm.org/doi/abs/10.1145/3408998 c.f. last paragraph of 4.1.  
> **username_0**: And [this paper](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/9A47A8663CD8A7147E2F17865C368094/S0960129521000487a.pdf/two_decades_of_automatic_amortized_resource_analysis.pdf) talks about the use of A-normal form in a preprocessing step before type checking, c.f. the bottom of page 7.  
> **username_2**: Simplicity: the logical rules become a tiny bit simpler when the arguments to all interesting operations in the ambient language are  trivial (constants or variables). If you allow full expressions, e.g. $M + N$ instead of, e.g., $x+y$ or $2 + 7$, then the logical rules also need to cater for the evaluation of $M$ and of $M$, and for every operation.  

---

## 0 answers

