PLC is widely used in the field of automatic control. The correctness verification methods of PLC programs include software model checking and theorem proving, etc. To use formal methods verifying the correctness of PLC programs, denotational semantics needs to define and then PLC programs can be modeled, model checking and verified. Based on the extended λ-calculus definition, the paper has researched and defined the architecture and denotational semantics of PLC programs. The work is the basis of model checking and theorem proving for correctness verification on PLC programs.