The purpose of this contribution is to give a coherent account of a particular narrative which links locales, geometric theories, sheaf semantics and constructive commutative algebra. We are hoping to convey a firm grasp of three ideas: (1) Locales are a kind of space in which opens instead of points are fundamental. (2) Sheaf semantics allows us to explore mathematical objects from custom-tailored mathematical universes. (3) Without loss of generality, any reduced ring is a field.
G. Sambin提供了完备布尔代数的构造性版本。在这里，我们首先显示一些性质有关重叠代数：我们证明了重叠态射的概念对应于经典的地图保持任意连接;我们提供了一个描述的原子集为基础的重叠代数的语言形式的拓扑，从而给出了一个谓词性的特点离散locale;我们表明，一个集合的幂集是自由重叠代数join-generated从集合。然后，我们推广重叠代数和重叠态射的概念，以各种方式提供建设性的版本的类别的布尔代数与地图保持任意现有的连接。
A constructive approach to the double-categorical small object argument
Institute for Logic, Language and Computation, Universiteit van Amsterdam（逻辑、语言与计算研究所，阿姆斯特丹大学）；Department of Mathematics and Statistics, Masaryk University（数学与统计系，马萨里克大学）；Institute for Application-Oriented Knowledge Processing, Johannes Kepler University Linz（应用导向知识处理研究所，约翰内斯·开普勒大学林茨分校）
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
Mathematical Institute, University of Bern（伯尔尼大学数学研究所）；School of Computer Science, University of Birimingham（伯明翰大学计算机学院）；School of Computing, The Australian National University（澳大利亚国立大学计算学院）
Constructing Initial Algebras Using Inflationary Iteration
经典集合论中的Adámek的一个老定理通过序数上的超限迭代构造了充分共连续的内函子的初始代数。我们证明了一个新的版本，工程建设性的逻辑，使用“通货膨胀”迭代的大小概念，抽象的极限序数只是他们的传递性，定向和良好的基础属性。借用泰勒的建设性的序数处理，我们表明，存在的大小与上界的任何给定的签名的指数。由此可以得出结论，只要人们承认由于Streicher、Moerdijk、van den Berg和Palmgren而产生的弱选择形式（WISC），就有丰富的一类内函子可以应用新定理，并且已知它在许多种拓扑的内部构造性逻辑中成立。
