A well-known result due to J.T. Stafford asserts that a
stably free left module
M over the Weyl algebras
D=An(k) or
Bn(k)–where
k is a field of characteristic 0–with
![]()
is
free. The purpose of this paper is to present a new constructive proof of this result as well as an effective algorithm for the computation of bases of
M. This algorithm, based on the new constructive proofs [Hillebrand, A., Schmale, W., 2001. Towards an effective version of a theorem of Stafford. J. Symbolic Comput. 32, 699–716; Leykin, A., 2004. Algorithmic proofs of two theorems of Stafford. J. Symbolic Comput. 38, 1535–1550] of J.T. Stafford’s result on the number of generators of left ideals of
D, performs Gaussian elimination on the formal adjoint of the presentation matrix of
M. We show that J.T. Stafford’s result is a particular case of a more general one asserting that a
stably free left
D-module
M with
![]()
is
free, where
![]()
denotes the stable rank of a ring
D. This result is constructive if the stability of unimodular vectors with entries in
D can be tested. Finally, an algorithm which computes the left projective dimension of a general left
D-module
M defined by means of a finite
free resolution is presented. It allows us to check whether or not the left
D-module
M is
stably free.