This work focuses on the innocent-looking but not so easy issue of relating the two main approaches approaches to conversion for dependent types, namely the typed, judgmental (“MLTT-style”) one and the untyped, rewriting based (“Pure Type System-style”) one, by focusing on algorithmic presentations. The key insight is that because these presentations, inspired by the actual algorithms for deciding conversion, are very structured, they make it easier to relate the two approaches. This provides an interesting building block to decompose the gap between typed specifications, which are the most amenable to theoretical work, and implementations, such as that of Coq, that forego types to speed-up conversion checking.