In Artificial Intelligence, a crucial requirement is the ability to reason about actions and their effects on the environment. Traditional approaches which rely on classical logic suffer from a number of limitations such as semi-decidability, closed-world assumption, frame problem, and a lack of ability to cope with partial knowledge and dynamic environments. While many solutions have been proposed for these topics, difficulties and uncertainties remain, even in the latest papers. In this paper, we look at this issue from a proof-theoretical perspective and we describe the foundations for reasoning about action based on Constructive Type Theory.