Library
ff-css
Modules
35
Total LOC
6,208
Used by
ff-html, ff-html-examples
Deps
cubical-0.9, ff-generics, ff-json
Five selector-specificity traces feed a braced declaration with unit, color, animation, and transform values; projections connect them to a timing curve, unit scale, and skewed viewport containing columns, overlapping contours, and a scroll track.
Typed CSS cascade, values, and rendered transforms

ff-css

repository URL pending

Scope

ff-css formalizes a typed representation of CSS in Agda, centered on safe syntax, properties, and values. Its value layer covers animation, transforms, units, colors, filters, compositing, masking, images, generated content, scrolling, and layout-oriented areas such as tables, multicolumn content, and inline formatting. Common and loose specifications sit alongside the safe modules, making different degrees of structure explicit. Core definitions, metadata, instances, generic support, and rendering connect the domain descriptions to reusable encodings and output. The library uses ff-generics and ff-json within the project and is developed over Cubical Agda.

Most important results

The safe specification defines a typed property language and an extensive value vocabulary instead of reducing declarations to unstructured text. Specialized modules cover animation and transforms together with color, compositing, filtering, masking, and generated content. Additional modules capture unit-bearing values and layout concerns including inline, list, table, multicolumn, ruby, break, containment, and scroll behavior. Rendering, metadata, generic descriptions, and instances provide the surrounding machinery needed to consume those representations.

Library modules

35 checked modules

Select a module to inspect its generated Agda source view.

Skip to content

Agda libraries

ff-css

Typed CSS property declarations for checked HTML artifacts.

Library
ff-css
Modules
35
Total LOC
6208
Dependencies
cubical-0.9, ff-generics, ff-json
Typed CSS cascade, values, and rendered transformsFive selector-specificity traces feed a braced declaration with unit, color, animation, and transform values; projections connect them to a timing curve, unit scale, and skewed viewport containing columns, overlapping contours, and a scroll track.
Five selector-specificity traces feed a braced declaration with unit, color, animation, and transform values; projections connect them to a timing curve, unit scale, and skewed viewport containing columns, overlapping contours, and a scroll track.
OverviewModulesArticle

Scope

ff-css formalizes a typed representation of CSS in Agda, centered on safe syntax, properties, and values. Its value layer covers animation, transforms, units, colors, filters, compositing, masking, images, generated content, scrolling, and layout-oriented areas such as tables, multicolumn content, and inline formatting. Common and loose specifications sit alongside the safe modules, making different degrees of structure explicit. Core definitions, metadata, instances, generic support, and rendering connect the domain descriptions to reusable encodings and output. The library uses ff-generics and ff-json within the project and is developed over Cubical Agda.

Most important results

The safe specification defines a typed property language and an extensive value vocabulary instead of reducing declarations to unstructured text. Specialized modules cover animation and transforms together with color, compositing, filtering, masking, and generated content. Additional modules capture unit-bearing values and layout concerns including inline, list, table, multicolumn, ruby, break, containment, and scroll behavior. Rendering, metadata, generic descriptions, and instances provide the surrounding machinery needed to consume those representations.

Used by

Source browser

Modules

Read the full library article

ff-css is a Cubical Agda library for typed CSS property declarations.

It exists because typed HTML is much less useful if styling falls back to arbitrary raw strings. ff-css provides the CSS layer used by ff-html, replacing raw style text with checked property/value pairs where the formalization has coverage.

Library Shape

The public entry point is FF.CSS. The library mirrors the ff-html safety ladder:

  • FF.CSS.Core defines spec-parametric properties, values, declarations, and maps;
  • FF.CSS.Render renders valid declarations;
  • FF.CSS.Spec.Loose keeps stringly typed CSS;
  • FF.CSS.Spec.Common uses known property names with string values;
  • FF.CSS.Spec.Safe starts the MDN-backed typed reference;
  • FF.CSS.Metadata and FF.CSS.Generic connect the reference work to ff-json and ff-generics.

The first safe slice covers CSS-wide keywords, common numeric/unit atoms, colors, display, positioning, sizing, spacing, borders, text, flex, and grid track forms.

Coverage

The property ledger tracks 492 standard CSS property pages from an MDN data snapshot dated 2026-06-14. At that snapshot:

  • 257 properties were exact;
  • 12 were partial;
  • 72 used an opaque property-specific wrapper for a deferred nested grammar;
  • 151 were still pending.

The page should present those numbers as coverage of typed declarations, not as browser semantics. Selectors, rules, stylesheets, cascade behavior, and parsing are outside ff-css; stylesheet work happens in the ff-html selector/stylesheet layer.

How It Fits

ff-css is the style-declaration layer for typed web artifacts. It gives ff-html a route away from raw style strings while keeping incomplete CSS coverage honest.

Web documents are a useful artifact surface for Formal Foundry: generated dashboards, documentation pages, component galleries, and proof-derived reports. If the structure is checked while the styles remain opaque text, the boundary is weaker than it needs to be.

The safe/common/loose ladder lets generated pages become more precise over time. A page can begin with broad compatibility and move specific properties into checked representations as coverage grows.

The coverage ledger is part of the value. It says which declarations are exact, which are partial, which use opaque wrappers, and which remain pending. That makes the CSS work inspectable rather than overclaimed.

The public message is practical: generated web surfaces can be checked at more than one layer. The structure can be typed, attributes can be tracked, and style declarations can gradually move from raw strings to explicit values.

Browse modulesOpen generated Agda sources

Cabinet index

Explore Formal Foundry

Book a meeting Explore libraries

Trusted systems. Mathematical proofs.

Search the archive

Find a page

Type to search the published content.