Nesting probabilistic programs is a powerful mechanism to express metareasoning and planning problems. Nested Inference, however, is a challenging task because of both tractability and formalization issues. In this work, we propose to perform exact (nested) inference for nested discrete probabilistic programs through an operational semantics based on probabilistic pushdown automata. Thereby, nested inference is reduced to solving a monotone system of polynomial equations. We report on some preliminary experimental results comparing our approach with the probabilistic programming language WebPPL.