Cryptic crossword with a theoretical computer science theme. Enjoy!

no14

Across
1 14d Bank managing a museum exhibiting bad art? (7,10)
5 17d Smooth ways of talking, readily accepted. (7,9)
9 Number system used around the end of the year? (3)
10 Kept by virtuous diarists and, one hopes, research libraries even after cutbacks. (4,7)
11 Headless monsters may be off by one. (6)
12 Repository hosting 18 down introductions explaining semantics and verification. (4)
13 King’s writ, maybe a quill. (2)
16 Good idea when checking if string argument has zero length; otherwise result oft not OK when k goes left. (4,3,4,3)
19 Cunningly silences top men in foundations of mathematics, such as Gödel’s most important contribution. (14)
21 God is in the particulars more than in the details. (2)
22 Architecture sounds like a gamble. (4)
24 Plutoniom store added on top of the others. (6)
27 Arbitrary model in statistical mechanics often improves bound on worst-case behaviour, at least in expectation. (11)
28 Apply resolution to a Horn clause. (3)
29 Author of election scheme and determinant 3 down (following 6 down) and connoisseur of acrostics did often draft good stories on nonsense! (7)
30 The simplest sets, i.e., a partial order. (7)

Down
1 Go from place to place in the pursuit of pleasure to understand a complicated construction in an NP-hardness reduction. (6)
2 8 Frequently visiting mother-in-law, for instance, can be a difficult challenge. (10,8)
3 Preparing for the oral might be a good strategy. (9)
4 Very long narrative in retrospect sounds like the specification of a structured information exchange protocol for web services. (4)
5 About first Java class compiled at even update. (10)
6 German summer takes the edges off temper, laid back. (5)
7 Favourite reference in many lists: My name is Bond. (4)
8 See 2 down.
14 See 1 across.
15 Building with supplies for Spooner’s unique key partner, where tea is served for a penny. (5,5)
17 See 5 across.
18 Becomes partly colder or rimed when applied to itself. (8)
20 Development to release after many years. (6)
23 First person to attach the head to statues. (5)
25 Where most computational geometry problems are easily solved, e.g., done by convolution. (3,1)
26 Type of French lady with compiler for high level programming language developed by the US Department of Defence. (4)