diff --git a/pkg/corset/binding.go b/pkg/corset/binding.go
index 6ab21b0..5af03eb 100644
--- a/pkg/corset/binding.go
+++ b/pkg/corset/binding.go
@@ -44,9 +44,21 @@ type ColumnBinding struct {
 	dataType Type
 }
 
-// NewColumnBinding constructs a new column binding in a given module.
-func NewColumnBinding(module string, computed bool, mustProve bool, multiplier uint, datatype Type) *ColumnBinding {
-	return &ColumnBinding{math.MaxUint, module, computed, mustProve, multiplier, datatype}
+// NewInputColumnBinding constructs a new column binding in a given module.
+// This is for the case where all information about the column is already known,
+// and will not be inferred from elsewhere.
+func NewInputColumnBinding(module string, mustProve bool, multiplier uint, datatype Type) *ColumnBinding {
+	return &ColumnBinding{math.MaxUint, module, false, mustProve, multiplier, datatype}
+}
+
+// NewComputedColumnBinding constructs a new column binding in a given
+// module.  This is for the case where not all information is yet known about
+// the column and, hence, it must be finalised later on.  For example, in a
+// definterleaved constraint the target column information (e.g. its type) is
+// not immediately available and must be determined from those columns from
+// which it is constructed.
+func NewComputedColumnBinding(module string) *ColumnBinding {
+	return &ColumnBinding{math.MaxUint, module, true, false, 0, nil}
 }
 
 // IsFinalised checks whether this binding has been finalised yet or not.
@@ -127,15 +139,15 @@ type ParameterBinding struct {
 	datatype Type
 }
 
-// ============================================================================
-// FunctionBinding
-// ============================================================================
-
 // IsFinalised checks whether this binding has been finalised yet or not.
 func (p *ParameterBinding) IsFinalised() bool {
-	panic("")
+	panic("should be unreachable?")
 }
 
+// ============================================================================
+// FunctionBinding
+// ============================================================================
+
 // FunctionBinding represents the binding of a function application to its
 // physical definition.
 type FunctionBinding struct {
diff --git a/pkg/corset/ast.go b/pkg/corset/declaration.go
similarity index 80%
rename from pkg/corset/ast.go
rename to pkg/corset/declaration.go
index f23e77b..3db55f5 100644
--- a/pkg/corset/ast.go
+++ b/pkg/corset/declaration.go
@@ -42,6 +42,11 @@ type Declaration interface {
 	Definitions() util.Iterator[SymbolDefinition]
 	// Return set of columns on which this declaration depends.
 	Dependencies() util.Iterator[Symbol]
+	// Check whether this declaration defines a given symbol.  The symbol in
+	// question needs to have been resolved already for this to make sense.
+	Defines(Symbol) bool
+	// Check whether this declaration is finalised already.
+	IsFinalised() bool
 }
 
 // ============================================================================
@@ -70,6 +75,20 @@ func (p *DefAliases) Definitions() util.Iterator[SymbolDefinition] {
 	return util.NewArrayIterator[SymbolDefinition](nil)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefAliases) Defines(symbol Symbol) bool {
+	// fine beause defaliases gets special treatement.
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefAliases) IsFinalised() bool {
+	// Fine because defaliases doesn't really do anything with its symbols.
+	return true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 //
@@ -130,6 +149,24 @@ func (p *DefColumns) Definitions() util.Iterator[SymbolDefinition] {
 	return util.NewCastIterator[*DefColumn, SymbolDefinition](iter)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefColumns) Defines(symbol Symbol) bool {
+	for _, sym := range p.Columns {
+		if &sym.binding == symbol.Binding() {
+			return true
+		}
+	}
+	//
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefColumns) IsFinalised() bool {
+	return true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefColumns) Lisp() sexp.SExp {
@@ -258,6 +295,30 @@ func (p *DefConst) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator[Symbol](deps)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefConst) Defines(symbol Symbol) bool {
+	for _, sym := range p.constants {
+		if &sym.binding == symbol.Binding() {
+			return true
+		}
+	}
+	//
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefConst) IsFinalised() bool {
+	for _, c := range p.constants {
+		if !c.binding.IsFinalised() {
+			return false
+		}
+	}
+	//
+	return true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefConst) Lisp() sexp.SExp {
@@ -338,6 +399,8 @@ type DefConstraint struct {
 	// The constraint itself which (when active) should evaluate to zero for the
 	// relevant set of rows.
 	Constraint Expr
+	//
+	finalised bool
 }
 
 // Definitions returns the set of symbols defined by this declaration.  Observe
@@ -359,6 +422,24 @@ func (p *DefConstraint) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator[Symbol](append(guard_deps, body_deps...))
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefConstraint) Defines(symbol Symbol) bool {
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefConstraint) IsFinalised() bool {
+	return p.finalised
+}
+
+// Finalise this declaration, which means that its guard (if applicable) and
+// body have been resolved.
+func (p *DefConstraint) Finalise() {
+	p.finalised = true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefConstraint) Lisp() sexp.SExp {
@@ -399,6 +480,8 @@ type DefInRange struct {
 	// an fr.Element is used here to store the bound simply to make the
 	// necessary comparison against table data more direct.
 	Bound fr.Element
+	// Indicates whether or not the expression has been resolved.
+	finalised bool
 }
 
 // Definitions returns the set of symbols defined by this declaration.  Observe
@@ -412,6 +495,23 @@ func (p *DefInRange) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator[Symbol](p.Expr.Dependencies())
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefInRange) Defines(symbol Symbol) bool {
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefInRange) IsFinalised() bool {
+	return p.finalised
+}
+
+// Finalise this declaration, meaning that the expression has been resolved.
+func (p *DefInRange) Finalise() {
+	p.finalised = true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefInRange) Lisp() sexp.SExp {
@@ -453,6 +553,18 @@ func (p *DefInterleaved) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator(p.Sources)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefInterleaved) Defines(symbol Symbol) bool {
+	return &p.Target.binding == symbol.Binding()
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefInterleaved) IsFinalised() bool {
+	return p.Target.binding.IsFinalised()
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefInterleaved) Lisp() sexp.SExp {
@@ -495,6 +607,8 @@ type DefLookup struct {
 	// Target expressions for lookup (i.e. these values must contain all of the
 	// source values, but may contain more).
 	Targets []Expr
+	// Indicates whether or not target and source expressions have been resolved.
+	finalised bool
 }
 
 // Definitions returns the set of symbols defined by this declaration.  Observe
@@ -511,6 +625,24 @@ func (p *DefLookup) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator(append(sourceDeps, targetDeps...))
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefLookup) Defines(symbol Symbol) bool {
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefLookup) IsFinalised() bool {
+	return p.finalised
+}
+
+// Finalise this declaration, which means that all source and target expressions
+// have been resolved.
+func (p *DefLookup) Finalise() {
+	p.finalised = true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefLookup) Lisp() sexp.SExp {
@@ -559,6 +691,30 @@ func (p *DefPermutation) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator(p.Sources)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefPermutation) Defines(symbol Symbol) bool {
+	for _, col := range p.Targets {
+		if &col.binding == symbol.Binding() {
+			return true
+		}
+	}
+	// Done
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefPermutation) IsFinalised() bool {
+	for _, col := range p.Targets {
+		if !col.binding.IsFinalised() {
+			return false
+		}
+	}
+	// Done
+	return true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefPermutation) Lisp() sexp.SExp {
@@ -606,6 +762,8 @@ type DefProperty struct {
 	// The assertion itself which (when active) should evaluate to zero for the
 	// relevant set of rows.
 	Assertion Expr
+	// Indicates whether or not the assertion has been resolved.
+	finalised bool
 }
 
 // Definitions returns the set of symbols defined by this declaration.  Observe that
@@ -619,6 +777,23 @@ func (p *DefProperty) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator(p.Assertion.Dependencies())
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefProperty) Defines(symbol Symbol) bool {
+	return false
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefProperty) IsFinalised() bool {
+	return p.finalised
+}
+
+// Finalise this property, meaning that the assertion has been resolved.
+func (p *DefProperty) Finalise() {
+	p.finalised = true
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefProperty) Lisp() sexp.SExp {
@@ -703,6 +878,18 @@ func (p *DefFun) Dependencies() util.Iterator[Symbol] {
 	return util.NewArrayIterator(ndeps)
 }
 
+// Defines checks whether this declaration defines the given symbol.  The symbol
+// in question needs to have been resolved already for this to make sense.
+func (p *DefFun) Defines(symbol Symbol) bool {
+	return &p.binding == symbol.Binding()
+}
+
+// IsFinalised checks whether this declaration has already been finalised.  If
+// so, then we don't need to finalise it again.
+func (p *DefFun) IsFinalised() bool {
+	return p.binding.IsFinalised()
+}
+
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefFun) Lisp() sexp.SExp {
@@ -737,5 +924,5 @@ type DefParameter struct {
 // Lisp converts this node into its lisp representation.  This is primarily used
 // for debugging purposes.
 func (p *DefParameter) Lisp() sexp.SExp {
-	panic("got here")
+	return sexp.NewSymbol(p.Name)
 }
diff --git a/pkg/corset/expr.go b/pkg/corset/expression.go
similarity index 100%
rename from pkg/corset/expr.go
rename to pkg/corset/expression.go
diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go
index ddfdd93..37690a7 100644
--- a/pkg/corset/parser.go
+++ b/pkg/corset/parser.go
@@ -316,7 +316,8 @@ func (p *Parser) parseDefColumns(module string, l *sexp.List) (Declaration, []Sy
 	var errors []SyntaxError
 	// Process column declarations one by one.
 	for i := 1; i < len(l.Elements); i++ {
-		decl, err := p.parseColumnDeclaration(module, l.Elements[i])
+		binding := NewInputColumnBinding(module, false, 1, NewFieldType())
+		decl, err := p.parseColumnDeclaration(l.Elements[i], binding)
 		// Extract column name
 		if err != nil {
 			errors = append(errors, *err)
@@ -332,10 +333,8 @@ func (p *Parser) parseDefColumns(module string, l *sexp.List) (Declaration, []Sy
 	return &DefColumns{columns}, nil
 }
 
-func (p *Parser) parseColumnDeclaration(module string, e sexp.SExp) (*DefColumn, *SyntaxError) {
+func (p *Parser) parseColumnDeclaration(e sexp.SExp, binding *ColumnBinding) (*DefColumn, *SyntaxError) {
 	var name string
-	//
-	binding := NewColumnBinding(module, false, false, 1, NewFieldType())
 	// Check whether extended declaration or not.
 	if l := e.AsList(); l != nil {
 		// Check at least the name provided.
@@ -432,7 +431,7 @@ func (p *Parser) parseDefConstraint(elements []sexp.SExp) (Declaration, []Syntax
 		return nil, errors
 	}
 	// Done
-	return &DefConstraint{elements[1].AsSymbol().Value, domain, guard, expr}, nil
+	return &DefConstraint{elements[1].AsSymbol().Value, domain, guard, expr, false}, nil
 }
 
 // Parse a interleaved declaration
@@ -457,7 +456,7 @@ func (p *Parser) parseDefInterleaved(module string, elements []sexp.SExp) (Decla
 		p.mapSourceNode(ith, sources[i])
 	}
 	//
-	binding := NewColumnBinding(module, false, false, 1, NewFieldType())
+	binding := NewComputedColumnBinding(module)
 	target := &DefColumn{elements[1].AsSymbol().Value, *binding}
 	// Updating mapping for target definition
 	p.mapSourceNode(elements[1], target)
@@ -499,7 +498,7 @@ func (p *Parser) parseDefLookup(elements []sexp.SExp) (Declaration, *SyntaxError
 		}
 	}
 	// Done
-	return &DefLookup{handle, sources, targets}, nil
+	return &DefLookup{handle, sources, targets, false}, nil
 }
 
 // Parse a permutation declaration
@@ -525,7 +524,8 @@ func (p *Parser) parseDefPermutation(module string, elements []sexp.SExp) (Decla
 	//
 	for i := 0; i < len(targets); i++ {
 		// Parse target column
-		if targets[i], err = p.parseColumnDeclaration(module, sexpTargets.Get(i)); err != nil {
+		binding := NewComputedColumnBinding(module)
+		if targets[i], err = p.parseColumnDeclaration(sexpTargets.Get(i), binding); err != nil {
 			return nil, err
 		}
 		// Parse source column
@@ -595,7 +595,7 @@ func (p *Parser) parseDefProperty(elements []sexp.SExp) (Declaration, *SyntaxErr
 		return nil, err
 	}
 	// Done
-	return &DefProperty{handle, expr}, nil
+	return &DefProperty{handle, expr, false}, nil
 }
 
 // Parse a permutation declaration
diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go
index 064349b..a2611e9 100644
--- a/pkg/corset/resolver.go
+++ b/pkg/corset/resolver.go
@@ -4,7 +4,6 @@ import (
 	"fmt"
 
 	"github.com/consensys/go-corset/pkg/sexp"
-	"github.com/consensys/go-corset/pkg/util"
 )
 
 // ResolveCircuit resolves all symbols declared and used within a circuit,
@@ -183,20 +182,24 @@ func (r *resolver) finaliseDeclarationsInModule(scope *ModuleScope, decls []Decl
 		complete = true
 		//
 		for _, d := range decls {
-			ready, errs := r.declarationDependenciesAreFinalised(scope, d.Dependencies())
-			// See what arosed
-			if errs != nil {
-				errors = append(errors, errs...)
-			} else if ready {
-				// Finalise declaration and handle errors
-				errs := r.finaliseDeclaration(scope, d)
-				errors = append(errors, errs...)
-				// Record that a new assignment is available.
-				changed = changed || len(errs) == 0
-			} else {
-				// Declaration not ready yet
-				complete = false
-				incomplete = d
+			// Check whether already finalised
+			if !d.IsFinalised() {
+				// No, so attempt to finalise
+				ready, errs := r.declarationDependenciesAreFinalised(scope, d)
+				// Check what we found
+				if errs != nil {
+					errors = append(errors, errs...)
+				} else if ready {
+					// Finalise declaration and handle errors
+					errs := r.finaliseDeclaration(scope, d)
+					errors = append(errors, errs...)
+					// Record that a new assignment is available.
+					changed = changed || len(errs) == 0
+				} else {
+					// Declaration not ready yet
+					complete = false
+					incomplete = d
+				}
 			}
 		}
 		// Sanity check for any errors caught during this iteration.
@@ -224,22 +227,30 @@ func (r *resolver) finaliseDeclarationsInModule(scope *ModuleScope, decls []Decl
 // since we cannot finalise a declaration until all of its dependencies have
 // themselves been finalised.
 func (r *resolver) declarationDependenciesAreFinalised(scope *ModuleScope,
-	symbols util.Iterator[Symbol]) (bool, []SyntaxError) {
+	decl Declaration) (bool, []SyntaxError) {
 	var (
 		errors    []SyntaxError
 		finalised bool = true
 	)
 	//
-	for iter := symbols; iter.HasNext(); {
+	for iter := decl.Dependencies(); iter.HasNext(); {
 		symbol := iter.Next()
 		// Attempt to resolve
 		if !symbol.IsResolved() && !scope.Bind(symbol) {
 			errors = append(errors, *r.srcmap.SyntaxError(symbol, "unknown symbol"))
 			// not finalised yet
 			finalised = false
-		} else if symbol.IsResolved() && !symbol.Binding().IsFinalised() {
-			// no, not finalised
-			finalised = false
+		} else {
+			// Check whether this declaration defines this symbol (because if it
+			// does, we cannot expect it to be finalised yet :)
+			selfdefinition := decl.Defines(symbol)
+			// Check whether this symbol is already finalised.
+			symbol_finalised := symbol.Binding().IsFinalised()
+			// Final check
+			if !selfdefinition && !symbol_finalised {
+				// Ok, not ready for finalisation yet.
+				finalised = false
+			}
 		}
 	}
 	//
@@ -278,13 +289,16 @@ func (r *resolver) finaliseDefConstInModule(enclosing Scope, decl *DefConst) []S
 	for _, c := range decl.constants {
 		scope := NewLocalScope(enclosing, false, true)
 		// Resolve constant body
-		_, errs := r.finaliseExpressionInModule(scope, c.binding.value)
+		datatype, errs := r.finaliseExpressionInModule(scope, c.binding.value)
 		// Accumulate errors
 		errors = append(errors, errs...)
 		// Check it is indeed constant!
 		if constant := c.binding.value.AsConstant(); constant == nil {
 			err := r.srcmap.SyntaxError(c, "definition not constant")
 			errors = append(errors, *err)
+		} else {
+			// Finalise constant binding
+			c.binding.Finalise(datatype)
 		}
 	}
 	//
@@ -316,6 +330,9 @@ func (r *resolver) finaliseDefConstraintInModule(enclosing Scope, decl *DefConst
 		msg := fmt.Sprintf("expected loobean constraint (found %s)", constraint_t.String())
 		err := r.srcmap.SyntaxError(decl.Constraint, msg)
 		errors = append(errors, *err)
+	} else if len(errors) == 0 {
+		// Finalise declaration.
+		decl.Finalise()
 	}
 	// Done
 	return append(guard_errors, errors...)
diff --git a/pkg/corset/scope.go b/pkg/corset/scope.go
index caa6ddc..3d042af 100644
--- a/pkg/corset/scope.go
+++ b/pkg/corset/scope.go
@@ -135,7 +135,7 @@ func (p *ModuleScope) Bind(symbol Symbol) bool {
 		binding := p.bindings[bid]
 		// Resolve symbol
 		return symbol.Resolve(binding)
-	} else if p.module != "" {
+	} else if !symbol.IsQualified() && p.module != "" {
 		// Attempt to lookup in parent (unless we are the root module, in which
 		// case we have no parent)
 		return p.enclosing.Bind(symbol)
diff --git a/pkg/corset/symbol.go b/pkg/corset/symbol.go
index c8a7ed5..d1109b7 100644
--- a/pkg/corset/symbol.go
+++ b/pkg/corset/symbol.go
@@ -1,6 +1,10 @@
 package corset
 
-import "github.com/consensys/go-corset/pkg/sexp"
+import (
+	"fmt"
+
+	"github.com/consensys/go-corset/pkg/sexp"
+)
 
 // Symbol represents a variable or function access within a declaration.
 // Initially, such the proper interpretation of such accesses is unclear and it
@@ -30,6 +34,15 @@ type Symbol interface {
 	Resolve(Binding) bool
 }
 
+// QualifiedName returns the qualified name of a given symbol
+func QualifiedName(symbol Symbol) string {
+	if symbol.IsQualified() {
+		return fmt.Sprintf("%s.%s", symbol.Module(), symbol.Name())
+	}
+	//
+	return symbol.Name()
+}
+
 // SymbolDefinition represents a declaration (or part thereof) which defines a
 // particular symbol.  For example, "defcolumns" will define one or more symbols
 // representing columns, etc.